Orthogonal sums of finite families of integral lattices

For a finite family of integral lattices L i in rational vector spaces V i, the orthogonal sum ⊥ i, L i is the integral lattice in Π i, V i whose carrier consists of the families with x i ∈ L i for every i, and whose form is the sum of the coordinate forms,

B(x, y) = ∑ i, L_i(x i, y i).

This is the ι-indexed analogue of the binary orthogonal sum TauCeti.IntegralLattice.orthogonalSum, and the lattice-level counterpart of the orthogonal sum TauCeti.FiniteQuadraticModule.pi of finite quadratic modules. Unlike a coordinate power, the summands may live in different ambient spaces: this is the shape of an orthogonal sum of root lattices of an ordered list of Dynkin components, indexed by Fin n, as used in gluing constructions of lattices. The coordinate power TauCeti.IntegralLattice.coordinatePower is the orthogonal sum of a constant family.

The orthogonal sum is nondegenerate when every summand is, and it is even, respectively positive definite, exactly when every summand is. Its rank is the sum of the ranks. It is functorial in the summands and invariant under reindexing the family, which is how a permutation of the components of a reducible root system acts on the orthogonal sum of their root lattices.

Main declarations

• TauCeti.IntegralLattice.piForm: the summed ambient form on Π i, V i.
• TauCeti.IntegralLattice.pi: the orthogonal sum of a finite family of integral lattices.
• TauCeti.IntegralLattice.isEven_pi_iff, TauCeti.IntegralLattice.isPosDef_pi_iff: evenness and positive-definiteness are detected summandwise.
• TauCeti.IntegralLattice.finrank_pi: the rank of the orthogonal sum is the sum of the ranks.
• TauCeti.IntegralLattice.Isometry.pi: the orthogonal sum of a family of isometries.
• TauCeti.IntegralLattice.Isometry.piCongrLeft: the isometry ⊥ k, L (σ k) ≅ ⊥ i, L i induced by an equivalence σ : κ ≃ ι of index types.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §3.
• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCeti/LinearAlgebra/IntegralLattice/CoordinatePower.lean: the coordinate power L^ι, the constant-family case pi fun _ : ι ↦ L.

The summed form

def TauCeti.IntegralLattice.piForm {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) : LinearMap.BilinForm ℚ ((i : ι) → V i)

The ambient form of an orthogonal sum: the sum of the pairings of corresponding coordinates.

@[simp]

theorem TauCeti.IntegralLattice.piForm_apply {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) (x y : (i : ι) → V i) : ((piForm L) x) y = ∑ i : ι, ((L i).form (x i)) (y i)

Evaluation of the orthogonal-sum form is the sum of the coordinate pairings.

theorem TauCeti.IntegralLattice.piForm_single_right {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) [DecidableEq ι] (x : (i : ι) → V i) (i : ι) (v : V i) : ((piForm L) x) (Pi.single i v) = ((L i).form (x i)) v

Pairing with a family supported at one index extracts that coordinate pairing.

theorem TauCeti.IntegralLattice.piForm_single_left {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) [DecidableEq ι] (i : ι) (v : V i) (y : (i : ι) → V i) : ((piForm L) (Pi.single i v)) y = ((L i).form v) (y i)

Pairing a family supported at one index with an arbitrary family extracts that coordinate pairing.

The orthogonal sum

def TauCeti.IntegralLattice.pi {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) : IntegralLattice ((i : ι) → V i)

The orthogonal sum of a finite family of integral lattices: the integral lattice in Π i, V i whose carrier consists of the families with x i ∈ L i for every i, with the summed form ∑ i, L_i(x i, y i).

@[simp]

theorem TauCeti.IntegralLattice.pi_carrier {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) : (pi L).carrier = Submodule.pi Set.univ fun (i : ι) => (L i).carrier

The carrier of an orthogonal sum consists of the families with values in the summands.

@[simp]

theorem TauCeti.IntegralLattice.pi_form {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) : (pi L).form = piForm L

The form of an orthogonal sum is the summed coordinate form.

theorem TauCeti.IntegralLattice.mem_pi_carrier_iff {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) (x : (i : ι) → V i) : x ∈ (pi L).carrier ↔ ∀ (i : ι), x i ∈ (L i).carrier

A family lies in the orthogonal sum exactly when each of its values lies in its summand.

theorem TauCeti.IntegralLattice.single_mem_pi_carrier {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) [DecidableEq ι] (i : ι) {v : V i} (hv : v ∈ (L i).carrier) : Pi.single i v ∈ (pi L).carrier

A family supported at one index, with value in that summand, lies in the orthogonal sum.

@[simp]

theorem TauCeti.IntegralLattice.norm_pi_apply {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) (x : (i : ι) → V i) : (pi L).norm x = ∑ i : ι, (L i).norm (x i)

The norm on an orthogonal sum is the sum of the coordinate norms.

theorem TauCeti.IntegralLattice.norm_pi_single {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) [DecidableEq ι] (i : ι) (x : V i) : (pi L).norm (Pi.single i x) = (L i).norm x

A vector supported in one summand has the norm it has in that summand.

Nondegeneracy

theorem TauCeti.IntegralLattice.nondegenerate_pi_iff {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) : (pi L).form.Nondegenerate ↔ ∀ (i : ι), (L i).form.Nondegenerate

The orthogonal-sum form is nondegenerate exactly when every summand form is.

instance TauCeti.IntegralLattice.instIsNondegeneratePi {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) [∀ (i : ι), (L i).IsNondegenerate] : (pi L).IsNondegenerate

An orthogonal sum of nondegenerate integral lattices is nondegenerate.

Evenness and positive-definiteness

@[simp]

theorem TauCeti.IntegralLattice.isEven_pi_iff {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) : (pi L).IsEven ↔ ∀ (i : ι), (L i).IsEven

An orthogonal sum is even exactly when every summand is even.

theorem TauCeti.IntegralLattice.isEven_pi {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] {L : (i : ι) → IntegralLattice (V i)} (hL : ∀ (i : ι), (L i).IsEven) : (pi L).IsEven

An orthogonal sum of even lattices is even.

@[simp]

theorem TauCeti.IntegralLattice.isPosDef_pi_iff {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) : (pi L).IsPosDef ↔ ∀ (i : ι), (L i).IsPosDef

An orthogonal sum is positive definite exactly when every summand is.

Rank

@[simp]

theorem TauCeti.IntegralLattice.finrank_pi {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) : Module.finrank ℤ ↥(pi L).carrier = ∑ i : ι, Module.finrank ℤ ↥(L i).carrier

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

Isometries

An orthogonal sum is functorial in its summands, and invariant under reindexing the family by an equivalence of index types. Reindexing is how a permutation of the components of a reducible root system acts on the orthogonal sum of their root lattices.

def TauCeti.IntegralLattice.Isometry.pi {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] {L : (i : ι) → IntegralLattice (V i)} {W : ι → Type w} [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℚ (W i)] {M : (i : ι) → IntegralLattice (W i)} (f : (i : ι) → (L i).Isometry (M i)) : (IntegralLattice.pi L).Isometry (IntegralLattice.pi M)

The orthogonal sum of a family of integral-lattice isometries, acting coordinatewise.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.pi_apply {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] {L : (i : ι) → IntegralLattice (V i)} {W : ι → Type w} [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℚ (W i)] {M : (i : ι) → IntegralLattice (W i)} (f : (i : ι) → (L i).Isometry (M i)) (x : (i : ι) → V i) (i : ι) : (pi f) x i = (f i) (x i)

The orthogonal sum of a family of isometries acts coordinatewise.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.pi_refl {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] {L : (i : ι) → IntegralLattice (V i)} : (pi fun (i : ι) => refl (L i)) = refl (IntegralLattice.pi L)

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

@[simp]

theorem TauCeti.IntegralLattice.Isometry.pi_symm {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] {L : (i : ι) → IntegralLattice (V i)} {W : ι → Type w} [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℚ (W i)] {M : (i : ι) → IntegralLattice (W i)} (f : (i : ι) → (L i).Isometry (M i)) : (pi f).symm = pi fun (i : ι) => (f i).symm

The inverse of an orthogonal sum of isometries is the orthogonal sum of the inverses.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.pi_trans {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] {L : (i : ι) → IntegralLattice (V i)} {W : ι → Type w} [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℚ (W i)] {M : (i : ι) → IntegralLattice (W i)} {X : ι → Type u_1} [(i : ι) → AddCommGroup (X i)] [(i : ι) → Module ℚ (X i)] {N : (i : ι) → IntegralLattice (X i)} (f : (i : ι) → (L i).Isometry (M i)) (g : (i : ι) → (M i).Isometry (N i)) : (pi f).trans (pi g) = pi fun (i : ι) => (f i).trans (g i)

Orthogonal sums of isometries preserve composition coordinatewise.

def TauCeti.IntegralLattice.Isometry.piCongrLeft {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) {κ : Type x} [Fintype κ] (σ : κ ≃ ι) : (IntegralLattice.pi fun (k : κ) => L (σ k)).Isometry (IntegralLattice.pi L)

Reindexing an orthogonal sum. An equivalence σ : κ ≃ ι of index types induces the isometry from the orthogonal sum of the reindexed family k ↦ L (σ k) to the orthogonal sum of L, moving the summand in position k to position σ k.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.piCongrLeft_apply_apply {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) {κ : Type x} [Fintype κ] (σ : κ ≃ ι) (x : (k : κ) → V (σ k)) (k : κ) : (piCongrLeft L σ) x (σ k) = x k

Reindexing an orthogonal sum moves the coordinate in position k to position σ k.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.piCongrLeft_symm_apply {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) {κ : Type x} [Fintype κ] (σ : κ ≃ ι) (y : (i : ι) → V i) (k : κ) : (piCongrLeft L σ).symm y k = y (σ k)

The inverse of reindexing an orthogonal sum reads the coordinate in position k from position σ k.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.piCongrLeft_refl {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) : piCongrLeft L (Equiv.refl ι) = refl (IntegralLattice.pi L)

Reindexing an orthogonal sum along the identity equivalence is the identity.

theorem TauCeti.IntegralLattice.Isometry.piCongrLeft_trans_pi {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) {W : ι → Type w} [(i : ι) → AddCommGroup (W i)] [(i : ι) → Module ℚ (W i)] {M : (i : ι) → IntegralLattice (W i)} {κ : Type x} [Fintype κ] (σ : κ ≃ ι) (f : (i : ι) → (L i).Isometry (M i)) : (piCongrLeft L σ).trans (pi f) = (pi fun (k : κ) => f (σ k)).trans (piCongrLeft M σ)

Reindexing commutes with orthogonal sums of isometries: reindexing and then applying f i in each position i agrees with applying f (σ k) in each position k and then reindexing.

def TauCeti.IntegralLattice.Isometry.piUnique {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) [Unique ι] : (IntegralLattice.pi L).Isometry (L default)

Evaluation is an isometry from a one-summand orthogonal sum to its sole summand.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.piUnique_apply {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) [Unique ι] (x : (i : ι) → V i) : (piUnique L) x = x default

The one-summand isometry evaluates at the unique index.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.piUnique_symm_apply {ι : Type v} [Fintype ι] {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) [Unique ι] (y : V default) : (piUnique L).symm y = uniqueElim y

The inverse one-summand isometry places a vector in the unique coordinate.