Documentation

TauCeti.LinearAlgebra.IntegralLattice.OrthogonalSum

Orthogonal sums of integral lattices #

The orthogonal sum has product carrier and block-diagonal form. This file constructs the lattice, its canonical carrier maps and product bases, and proves several invariant laws: rank is additive, Gram matrices are block diagonal, determinant and discriminant are multiplicative, and evenness and nondegeneracy are componentwise. Orthogonal sums are functorial under lattice isometries and are associative and commutative up to canonical lattice isometry. The radical is the product of the component radicals, and the signature is componentwise additive.

Main definitions #

TauCeti.IntegralLattice.orthogonalSumForm: the block-diagonal ambient form.
TauCeti.IntegralLattice.orthogonalSum: the orthogonal sum lattice.
TauCeti.IntegralLattice.orthogonalSumCarrierEquiv: the carrier-product equivalence.
TauCeti.IntegralLattice.orthogonalSumBasis: the product of two carrier bases.
TauCeti.IntegralLattice.signature_orthogonalSum: signature is additive componentwise.
TauCeti.IntegralLattice.Isometry.orthogonalSum: the product of two lattice isometries.
TauCeti.IntegralLattice.Isometry.orthogonalSumComm: the canonical commutativity isometry.
TauCeti.IntegralLattice.Isometry.orthogonalSumAssoc: the canonical associativity isometry.

References #

W. Ebeling, Lattices and Codes, Chapter 1.
TauCetiRoadmap/IntegralLattices/README.md, Layer 1.
The isometry constructions follow Mathlib's QuadraticMap.IsometryEquiv.prod and prodComm in Mathlib/LinearAlgebra/QuadraticForm/Prod.lean.

def TauCeti.IntegralLattice.orthogonalSumForm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

LinearMap.BilinForm ℚ (V × W)

The block-diagonal bilinear form on a product, with the two factors orthogonal.

Equations

L.orthogonalSumForm M = L.form.comp (LinearMap.fst ℚ V W) (LinearMap.fst ℚ V W) + M.form.comp (LinearMap.snd ℚ V W) (LinearMap.snd ℚ V W)

Instances For

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumForm_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p q : V × W) :

((L.orthogonalSumForm M) p) q = (L.form p.1) q.1 + (M.form p.2) q.2

Evaluation of the block-diagonal form is the sum of the component pairings.

def TauCeti.IntegralLattice.orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

IntegralLattice (V × W)

The orthogonal sum of two integral lattices.

Equations

L.orthogonalSum M = { carrier := L.carrier.prod M.carrier, form := L.orthogonalSumForm M, isLattice := ⋯, isSymm := ⋯, le_dual := ⋯ }

Instances For

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSum_carrier {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).carrier = L.carrier.prod M.carrier

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSum_form {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).form = L.orthogonalSumForm M

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumForm_toQuadraticMap {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

LinearMap.BilinMap.toQuadraticMap (L.orthogonalSumForm M) = (LinearMap.BilinMap.toQuadraticMap L.form).prod (LinearMap.BilinMap.toQuadraticMap M.form)

The quadratic map of the block-diagonal form is the product of the component quadratic maps.

def TauCeti.IntegralLattice.orthogonalSumCarrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

↥(L.orthogonalSum M).carrier ≃ₗ[ℤ ] ↥L.carrier × ↥M.carrier

The carrier of an orthogonal sum is canonically the product of the carrier types.

Equations

L.orthogonalSumCarrierEquiv M = LinearEquiv.ofEq (L.orthogonalSum M).carrier (L.carrier.prod M.carrier) ⋯ ≪≫ₗ L.carrier.prodEquiv M.carrier

Instances For

def TauCeti.IntegralLattice.orthogonalSumInl {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

↥L.carrier →ₗ[ℤ ] ↥(L.orthogonalSum M).carrier

The canonical inclusion of the first carrier into an orthogonal sum.

Equations

L.orthogonalSumInl M = { toFun := fun (a : ↥L.carrier) => ⟨(↑a, 0), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Instances For

def TauCeti.IntegralLattice.orthogonalSumInr {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

↥M.carrier →ₗ[ℤ ] ↥(L.orthogonalSum M).carrier

The canonical inclusion of the second carrier into an orthogonal sum.

Equations

L.orthogonalSumInr M = { toFun := fun (b : ↥M.carrier) => ⟨(0, ↑b), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Instances For

def TauCeti.IntegralLattice.orthogonalSumFst {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

↥(L.orthogonalSum M).carrier →ₗ[ℤ ] ↥L.carrier

The canonical first projection from the carrier of an orthogonal sum.

Equations

L.orthogonalSumFst M = LinearMap.fst ℤ ↥L.carrier ↥M.carrier ∘ₗ ↑(L.orthogonalSumCarrierEquiv M)

Instances For

def TauCeti.IntegralLattice.orthogonalSumSnd {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

↥(L.orthogonalSum M).carrier →ₗ[ℤ ] ↥M.carrier

The canonical second projection from the carrier of an orthogonal sum.

Equations

L.orthogonalSumSnd M = LinearMap.snd ℤ ↥L.carrier ↥M.carrier ∘ₗ ↑(L.orthogonalSumCarrierEquiv M)

Instances For

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumInl_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (a : ↥L.carrier) :

↑((L.orthogonalSumInl M) a) = (↑a, 0)

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumInr_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (b : ↥M.carrier) :

↑((L.orthogonalSumInr M) b) = (0, ↑b)

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumFst_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ↥(L.orthogonalSum M).carrier) :

(L.orthogonalSumFst M) p = ((L.orthogonalSumCarrierEquiv M) p).1

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumSnd_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ↥(L.orthogonalSum M).carrier) :

(L.orthogonalSumSnd M) p = ((L.orthogonalSumCarrierEquiv M) p).2

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumCarrierEquiv_inl {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (a : ↥L.carrier) :

(L.orthogonalSumCarrierEquiv M) ((L.orthogonalSumInl M) a) = (a, 0)

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumCarrierEquiv_inr {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (b : ↥M.carrier) :

(L.orthogonalSumCarrierEquiv M) ((L.orthogonalSumInr M) b) = (0, b)

theorem TauCeti.IntegralLattice.orthogonalSumFst_inl {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (a : ↥L.carrier) :

(L.orthogonalSumFst M) ((L.orthogonalSumInl M) a) = a

The first projection of the first inclusion is the identity.

theorem TauCeti.IntegralLattice.orthogonalSumFst_inr {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (b : ↥M.carrier) :

(L.orthogonalSumFst M) ((L.orthogonalSumInr M) b) = 0

The first projection of the second inclusion is zero.

theorem TauCeti.IntegralLattice.orthogonalSumSnd_inl {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (a : ↥L.carrier) :

(L.orthogonalSumSnd M) ((L.orthogonalSumInl M) a) = 0

The second projection of the first inclusion is zero.

theorem TauCeti.IntegralLattice.orthogonalSumSnd_inr {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (b : ↥M.carrier) :

(L.orthogonalSumSnd M) ((L.orthogonalSumInr M) b) = b

The second projection of the second inclusion is the identity.

@[simp]

theorem TauCeti.IntegralLattice.coe_orthogonalSumCarrierEquiv_fst {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ↥(L.orthogonalSum M).carrier) :

↑((L.orthogonalSumCarrierEquiv M) p).1 = (↑p).1

@[simp]

theorem TauCeti.IntegralLattice.coe_orthogonalSumCarrierEquiv_snd {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ↥(L.orthogonalSum M).carrier) :

↑((L.orthogonalSumCarrierEquiv M) p).2 = (↑p).2

theorem TauCeti.IntegralLattice.orthogonalSumInl_fst_add_inr_snd_eq {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ↥(L.orthogonalSum M).carrier) :

(L.orthogonalSumInl M) ((L.orthogonalSumFst M) p) + (L.orthogonalSumInr M) ((L.orthogonalSumSnd M) p) = p

A vector in an orthogonal sum is the sum of the inclusions of its two projections.

noncomputable def TauCeti.IntegralLattice.orthogonalSumBasis {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {I : Type w} {J : Type x} (L : IntegralLattice V) (M : IntegralLattice W) (e : Module.Basis I ℤ ↥L.carrier) (f : Module.Basis J ℤ ↥M.carrier) :

Module.Basis (I ⊕ J) ℤ ↥(L.orthogonalSum M).carrier

The product of carrier bases is a basis of the orthogonal sum carrier.

Equations

L.orthogonalSumBasis M e f = (e.prod f).map (L.orthogonalSumCarrierEquiv M).symm

Instances For

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumBasis_apply_inl {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {I : Type w} {J : Type x} (L : IntegralLattice V) (M : IntegralLattice W) (e : Module.Basis I ℤ ↥L.carrier) (f : Module.Basis J ℤ ↥M.carrier) (i : I) :

(L.orthogonalSumBasis M e f) (Sum.inl i) = (L.orthogonalSumInl M) (e i)

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumBasis_apply_inr {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {I : Type w} {J : Type x} (L : IntegralLattice V) (M : IntegralLattice W) (e : Module.Basis I ℤ ↥L.carrier) (f : Module.Basis J ℤ ↥M.carrier) (j : J) :

(L.orthogonalSumBasis M e f) (Sum.inr j) = (L.orthogonalSumInr M) (f j)

@[simp]

theorem TauCeti.IntegralLattice.integralForm_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p q : ↥(L.orthogonalSum M).carrier) :

((L.orthogonalSum M).integralForm p) q = (L.integralForm ((L.orthogonalSumFst M) p)) ((L.orthogonalSumFst M) q) + (M.integralForm ((L.orthogonalSumSnd M) p)) ((L.orthogonalSumSnd M) q)

The integral form of an orthogonal sum is the sum of its two component forms.

@[simp]

theorem TauCeti.IntegralLattice.integralNorm_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : ↥(L.orthogonalSum M).carrier) :

(L.orthogonalSum M).integralNorm p = L.integralNorm ((L.orthogonalSumFst M) p) + M.integralNorm ((L.orthogonalSumSnd M) p)

The integral norm of an orthogonal-sum vector is the sum of its component norms.

@[simp]

theorem TauCeti.IntegralLattice.finrank_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

Module.finrank ℤ ↥(L.orthogonalSum M).carrier = Module.finrank ℤ ↥L.carrier + Module.finrank ℤ ↥M.carrier

The rank of an orthogonal sum is the sum of the ranks.

theorem TauCeti.IntegralLattice.gramMatrix_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {I : Type w} {J : Type x} (L : IntegralLattice V) (M : IntegralLattice W) (e : Module.Basis I ℤ ↥L.carrier) (f : Module.Basis J ℤ ↥M.carrier) :

(L.orthogonalSum M).gramMatrix (L.orthogonalSumBasis M e f) = Matrix.fromBlocks (L.gramMatrix e) 0 0 (M.gramMatrix f)

In product bases, the Gram matrix of an orthogonal sum is block diagonal.

theorem TauCeti.IntegralLattice.gramDet_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {I : Type w} {J : Type x} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] (L : IntegralLattice V) (M : IntegralLattice W) (e : Module.Basis I ℤ ↥L.carrier) (f : Module.Basis J ℤ ↥M.carrier) :

(L.orthogonalSum M).gramDet (L.orthogonalSumBasis M e f) = L.gramDet e * M.gramDet f

The Gram determinant of an orthogonal sum in product bases is the product of the two Gram determinants.

@[simp]

theorem TauCeti.IntegralLattice.determinant_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).determinant = L.determinant * M.determinant

The signed determinant of an orthogonal sum is multiplicative.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).discriminant = L.discriminant * M.discriminant

The nonnegative discriminant of an orthogonal sum is multiplicative.

@[simp]

theorem TauCeti.IntegralLattice.isEven_orthogonalSum_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).IsEven ↔ L.IsEven ∧ M.IsEven

An orthogonal sum is even exactly when both summands are even.

@[simp]

theorem TauCeti.IntegralLattice.nondegenerate_orthogonalSumForm_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSumForm M).Nondegenerate ↔ L.form.Nondegenerate ∧ M.form.Nondegenerate

The block-diagonal form is nondegenerate exactly when both component forms are nondegenerate.

theorem TauCeti.IntegralLattice.nondegenerate_orthogonalSum_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).form.Nondegenerate ↔ L.form.Nondegenerate ∧ M.form.Nondegenerate

The ambient form of an orthogonal sum is nondegenerate exactly when both summand forms are.

instance TauCeti.IntegralLattice.instIsNondegenerateOrthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] :

(L.orthogonalSum M).IsNondegenerate

The orthogonal sum of two nondegenerate integral lattices is nondegenerate.

Radical and signature #

@[simp]

theorem TauCeti.IntegralLattice.radical_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).radical = L.radical.prod M.radical

The radical of an orthogonal sum is the product of the component radicals.

@[simp]

theorem TauCeti.IntegralLattice.sigPos_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).sigPos = L.sigPos + M.sigPos

The positive index of an orthogonal sum is the sum of the positive indices.

@[simp]

theorem TauCeti.IntegralLattice.sigNeg_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).sigNeg = L.sigNeg + M.sigNeg

The negative index of an orthogonal sum is the sum of the negative indices.

@[simp]

theorem TauCeti.IntegralLattice.sigNull_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).sigNull = L.sigNull + M.sigNull

The null index of an orthogonal sum is the sum of the null indices.

@[simp]

theorem TauCeti.IntegralLattice.signature_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).signature = (L.sigPos + M.sigPos, L.sigNull + M.sigNull, L.sigNeg + M.sigNeg)

The signature of an orthogonal sum is the componentwise sum of the two signatures.

Isometries of orthogonal sums #

def TauCeti.IntegralLattice.Isometry.orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} (f : L.Isometry L') (g : M.Isometry M') :

(L.orthogonalSum M).Isometry (L'.orthogonalSum M')

The orthogonal sum of two integral-lattice isometries.

Equations

f.orthogonalSum g = { toIsometryEquiv := let __LinearEquiv := f.prodCongr g.toLinearEquiv; { toLinearEquiv := __LinearEquiv, map_app' := ⋯ }, map_carrier := ⋯ }

Instances For

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSum_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} (f : L.Isometry L') (g : M.Isometry M') (p : V × W) :

(f.orthogonalSum g) p = (f p.1, g p.2)

The product isometry acts componentwise on the ambient product.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSum_carrierEquiv_inl {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} (f : L.Isometry L') (g : M.Isometry M') (a : ↥L.carrier) :

(f.orthogonalSum g).carrierEquiv ((L.orthogonalSumInl M) a) = (L'.orthogonalSumInl M') (f.carrierEquiv a)

Product isometries commute with the first canonical carrier inclusion.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSum_carrierEquiv_inr {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} (f : L.Isometry L') (g : M.Isometry M') (b : ↥M.carrier) :

(f.orthogonalSum g).carrierEquiv ((L.orthogonalSumInr M) b) = (L'.orthogonalSumInr M') (g.carrierEquiv b)

Product isometries commute with the second canonical carrier inclusion.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumCarrierEquiv_carrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} (f : L.Isometry L') (g : M.Isometry M') (p : ↥(L.orthogonalSum M).carrier) :

(L'.orthogonalSumCarrierEquiv M') ((f.orthogonalSum g).carrierEquiv p) = (f.carrierEquiv ((L.orthogonalSumFst M) p), g.carrierEquiv ((L.orthogonalSumSnd M) p))

Product isometries commute with the canonical carrier-product equivalence.

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumFst_carrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} (f : L.Isometry L') (g : M.Isometry M') (p : ↥(L.orthogonalSum M).carrier) :

(L'.orthogonalSumFst M') ((f.orthogonalSum g).carrierEquiv p) = f.carrierEquiv ((L.orthogonalSumFst M) p)

Product isometries commute with the first canonical carrier projection.

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumSnd_carrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} (f : L.Isometry L') (g : M.Isometry M') (p : ↥(L.orthogonalSum M).carrier) :

(L'.orthogonalSumSnd M') ((f.orthogonalSum g).carrierEquiv p) = g.carrierEquiv ((L.orthogonalSumSnd M) p)

Product isometries commute with the second canonical carrier projection.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSum_refl {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(refl L).orthogonalSum (refl M) = refl (L.orthogonalSum M)

The product of identity isometries is the identity of the orthogonal sum.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSum_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} (f : L.Isometry L') (g : M.Isometry M') :

(f.orthogonalSum g).symm = f.symm.orthogonalSum g.symm

The inverse of a product isometry is the product of the inverse isometries.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSum_trans {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} {U : Type y} {Z : Type z} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] [AddCommGroup U] [Module ℚ U] [AddCommGroup Z] [Module ℚ Z] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} {L'' : IntegralLattice U} {M'' : IntegralLattice Z} (f : L.Isometry L') (g : M.Isometry M') (f' : L'.Isometry L'') (g' : M'.Isometry M'') :

(f.orthogonalSum g).trans (f'.orthogonalSum g') = (f.trans f').orthogonalSum (g.trans g')

Product isometries preserve composition componentwise.

def TauCeti.IntegralLattice.Isometry.orthogonalSumComm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(L.orthogonalSum M).Isometry (M.orthogonalSum L)

Orthogonal sum is commutative up to the canonical factor-swapping lattice isometry.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumComm_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (p : V × W) :

(orthogonalSumComm L M) p = (p.2, p.1)

The commutativity isometry swaps the two ambient components.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumComm_carrierEquiv_inl {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (a : ↥L.carrier) :

(orthogonalSumComm L M).carrierEquiv ((L.orthogonalSumInl M) a) = (M.orthogonalSumInr L) a

The commutativity isometry exchanges the canonical carrier inclusions.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumComm_carrierEquiv_inr {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (b : ↥M.carrier) :

(orthogonalSumComm L M).carrierEquiv ((L.orthogonalSumInr M) b) = (M.orthogonalSumInl L) b

The commutativity isometry exchanges the canonical carrier inclusions.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumComm_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) :

(orthogonalSumComm L M).symm = orthogonalSumComm M L

The inverse commutativity isometry swaps the factors in the opposite order.

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumComm_naturality {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] {L : IntegralLattice V} {M : IntegralLattice W} {L' : IntegralLattice X} {M' : IntegralLattice Y} (f : L.Isometry L') (g : M.Isometry M') :

(f.orthogonalSum g).trans (orthogonalSumComm L' M') = (orthogonalSumComm L M).trans (g.orthogonalSum f)

The commutativity isometry is natural with respect to isometries of both factors.

def TauCeti.IntegralLattice.Isometry.orthogonalSumAssoc {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {U : Type y} [AddCommGroup U] [Module ℚ U] (L : IntegralLattice V) (M : IntegralLattice W) (N : IntegralLattice U) :

((L.orthogonalSum M).orthogonalSum N).Isometry (L.orthogonalSum (M.orthogonalSum N))

Orthogonal sum is associative up to the canonical reassociation lattice isometry.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumAssoc_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {U : Type y} [AddCommGroup U] [Module ℚ U] (L : IntegralLattice V) (M : IntegralLattice W) (N : IntegralLattice U) (p : (V × W) × U) :

(orthogonalSumAssoc L M N) p = (p.1.1, p.1.2, p.2)

The associativity isometry reassociates the three ambient components.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumAssoc_symm_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {U : Type y} [AddCommGroup U] [Module ℚ U] (L : IntegralLattice V) (M : IntegralLattice W) (N : IntegralLattice U) (p : V × W × U) :

(orthogonalSumAssoc L M N).symm p = ((p.1, p.2.1), p.2.2)

The inverse associativity isometry restores left-associated products.

theorem TauCeti.IntegralLattice.Isometry.orthogonalSumAssoc_naturality {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {X : Type w} {Y : Type x} {U : Type y} {Z : Type z} [AddCommGroup X] [Module ℚ X] [AddCommGroup Y] [Module ℚ Y] [AddCommGroup U] [Module ℚ U] [AddCommGroup Z] [Module ℚ Z] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} {L' : IntegralLattice X} {M' : IntegralLattice Y} {N' : IntegralLattice Z} (f : L.Isometry L') (g : M.Isometry M') (h : N.Isometry N') :

((f.orthogonalSum g).orthogonalSum h).trans (orthogonalSumAssoc L' M' N') = (orthogonalSumAssoc L M N).trans (f.orthogonalSum (g.orthogonalSum h))

The associativity isometry is natural with respect to isometries of all three factors.