Splitting off the vectors of norm one

Let L be a positive definite integral lattice. Two vectors of norm one are either equal up to sign or orthogonal, since B(x ∓ y, x ∓ y) = 2 ∓ 2 B(x, y) is positive unless x = ±y. Choosing one vector from each pair ±x therefore gives an orthonormal basis of the sublattice U spanned by the vectors of norm one, so U is a copy of the standard lattice I_k. Its pairing is perfect, so it splits off orthogonally:

L ≅ I_k ⊕ U^⊥,   2k = #{x ∈ L : B(x, x) = 1},

and the complement U^⊥ has no vector of norm one, because such a vector would lie in U and be orthogonal to itself. The complement is positive definite, has the same determinant as L, and is unimodular exactly when L is. This is the first reduction in the classification of positive definite unimodular lattices of small rank: every such lattice is I_k plus a lattice without vectors of norm one.

The splitting is canonical. An isometry L ≅ M restricts to an isometry of the complements, and a lattice of the form I_ι ⊕ N, with N positive definite without vectors of norm one, has complement isometric to N. Hence I_ι ⊕ N ≅ I_κ ⊕ N' with N, N' positive definite without vectors of norm one forces #ι = #κ and N ≅ N'.

Main declarations

• TauCeti.IntegralLattice.unitNormSubmodule: the span of the vectors of norm one.
• TauCeti.IntegralLattice.unitNormComplement: its orthogonal complement, as an integral lattice.
• TauCeti.IntegralLattice.IsPosDef.unitNormBasis: an orthonormal basis of the unit-norm sublattice of a positive definite lattice.
• TauCeti.IntegralLattice.IsPosDef.unitNormDecomposition: the isometry I_k ⊕ unitNormComplement L ≅ L.
• TauCeti.IntegralLattice.vectorsOfNorm_one_unitNormComplement: the complement has no vector of norm one.
• TauCeti.IntegralLattice.IsPosDef.two_mul_finrank_unitNormSubmodule: 2k is the number of vectors of norm one.
• TauCeti.IntegralLattice.two_le_finrank_unitNormSubmodule: two orthogonal vectors of norm one give 2 ≤ k.
• TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_unitLattice_of_unitNormSubmodule_eq_top: a positive definite lattice spanned by its vectors of norm one is I_n.
• TauCeti.IntegralLattice.Isometry.unitNormComplement: isometric lattices have isometric complements.
• TauCeti.IntegralLattice.nonempty_isometry_of_isometry_orthogonalSum_unitLattice and TauCeti.IntegralLattice.card_eq_of_isometry_orthogonalSum_unitLattice: cancellation of standard summands against lattices without vectors of norm one.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §82.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 16.

noncomputable def TauCeti.IntegralLattice.unitNormSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule ℤ ↥L.carrier

The unit-norm sublattice of an integral lattice: the span of its vectors of norm one.

theorem TauCeti.IntegralLattice.vectorsOfNorm_one_subset_unitNormSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.vectorsOfNorm 1 ⊆ ↑L.unitNormSubmodule

Every vector of norm one lies in the unit-norm sublattice.

theorem TauCeti.IntegralLattice.unitNormSubmodule_le_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {p : Submodule ℤ ↥L.carrier} : L.unitNormSubmodule ≤ p ↔ L.vectorsOfNorm 1 ⊆ ↑p

The unit-norm sublattice is the least submodule containing the vectors of norm one.

theorem TauCeti.IntegralLattice.two_le_finrank_unitNormSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {x y : ↥L.carrier} (hx : (L.integralForm x) x = 1) (hy : (L.integralForm y) y = 1) (hxy : (L.integralForm x) y = 0) : 2 ≤ Module.finrank ℤ ↥L.unitNormSubmodule

Two orthogonal vectors of norm one span a rank-two part of the unit-norm sublattice.

noncomputable def TauCeti.IntegralLattice.unitNormComplement {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : IntegralLattice (TensorProduct ℤ ℚ ↥(L.integralForm.orthogonal L.unitNormSubmodule))

The orthogonal complement of the unit-norm sublattice, as an integral lattice in its own rational span.

noncomputable def TauCeti.IntegralLattice.unitNormComplementEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ↥(L.integralForm.orthogonal L.unitNormSubmodule) ≃ₗ[ℤ] ↥L.unitNormComplement.carrier

The canonical identification of the orthogonal complement of the unit-norm sublattice with the carrier of unitNormComplement.

@[simp]

theorem TauCeti.IntegralLattice.coe_unitNormComplementEquiv_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥(L.integralForm.orthogonal L.unitNormSubmodule)) : ↑(L.unitNormComplementEquiv x) = 1 ⊗ₜ[ℤ] x

The identification unitNormComplementEquiv sends x to the pure tensor 1 ⊗ x.

@[simp]

theorem TauCeti.IntegralLattice.integralForm_unitNormComplementEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥(L.integralForm.orthogonal L.unitNormSubmodule)) : (L.unitNormComplement.integralForm (L.unitNormComplementEquiv x)) (L.unitNormComplementEquiv y) = (L.integralForm ↑x) ↑y

The identification unitNormComplementEquiv preserves the integral forms.

@[simp]

theorem TauCeti.IntegralLattice.vectorsOfNorm_one_unitNormComplement {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.unitNormComplement.vectorsOfNorm 1 = ∅

The complement of the unit-norm sublattice has no vector of norm one.

theorem TauCeti.IntegralLattice.IsPosDef.integralForm_eq_zero_of_mem_vectorsOfNorm_one {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) {x y : ↥L.carrier} (hx : x ∈ L.vectorsOfNorm 1) (hy : y ∈ L.vectorsOfNorm 1) (hxy : y ≠ x) (hxy' : y ≠ -x) : (L.integralForm x) y = 0

Vectors of norm one in a positive definite lattice are equal up to sign or orthogonal.

An orthonormal basis of the unit-norm sublattice

noncomputable def TauCeti.IntegralLattice.IsPosDef.unitNormBasis {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : Module.Basis (Fin (Module.finrank ℤ ↥L.unitNormSubmodule)) ℤ ↥L.unitNormSubmodule

The unit-norm sublattice of a positive definite lattice has an orthonormal basis, made of one vector from each pair ±x of vectors of norm one.

theorem TauCeti.IntegralLattice.IsPosDef.unitNormBasis_mem_vectorsOfNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (i : Fin (Module.finrank ℤ ↥L.unitNormSubmodule)) : ↑(hL.unitNormBasis i) ∈ L.vectorsOfNorm 1

The vectors of unitNormBasis have norm one.

theorem TauCeti.IntegralLattice.IsPosDef.integralForm_unitNormBasis {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (i j : Fin (Module.finrank ℤ ↥L.unitNormSubmodule)) : (L.integralForm ↑(hL.unitNormBasis i)) ↑(hL.unitNormBasis j) = if i = j then 1 else 0

The basis unitNormBasis is orthonormal.

theorem TauCeti.IntegralLattice.IsPosDef.two_mul_finrank_unitNormSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : 2 * Module.finrank ℤ ↥L.unitNormSubmodule = (L.vectorsOfNorm 1).ncard

Twice the rank of the unit-norm sublattice is the number of vectors of norm one.

theorem TauCeti.IntegralLattice.IsPosDef.bijective_integralForm_restrict_unitNormSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : Function.Bijective ⇑(L.integralForm.restrict L.unitNormSubmodule)

The unit-norm sublattice of a positive definite lattice is unimodular: its restricted integral pairing is perfect.

The splitting

noncomputable def TauCeti.IntegralLattice.IsPosDef.unitNormDecomposition {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : ((unitLattice (Fin (Module.finrank ℤ ↥L.unitNormSubmodule))).orthogonalSum L.unitNormComplement).Isometry L

A positive definite lattice is I_k plus a lattice without vectors of norm one. The standard lattice I_k is carried onto the unit-norm sublattice, with k its rank, and the second summand is the complement unitNormComplement L.

@[simp]

theorem TauCeti.IntegralLattice.IsPosDef.unitNormDecomposition_apply_single {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (i : Fin (Module.finrank ℤ ↥L.unitNormSubmodule)) : hL.unitNormDecomposition (Pi.single i 1, 0) = ↑↑(hL.unitNormBasis i)

The splitting sends the i-th coordinate vector of I_k to the i-th vector of the orthonormal basis unitNormBasis.

@[simp]

theorem TauCeti.IntegralLattice.IsPosDef.unitNormDecomposition_apply_zero_tmul {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (r : ℚ) (t : ↥(L.integralForm.orthogonal L.unitNormSubmodule)) : hL.unitNormDecomposition (0, r ⊗ₜ[ℤ] t) = r • ↑↑t

The splitting is the inclusion on the complement of the unit-norm sublattice.

theorem TauCeti.IntegralLattice.IsPosDef.isPosDef_unitNormComplement {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : L.unitNormComplement.IsPosDef

The complement of the unit-norm sublattice of a positive definite lattice is positive definite.

@[simp]

theorem TauCeti.IntegralLattice.IsPosDef.determinant_unitNormComplement {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : L.unitNormComplement.determinant = L.determinant

Splitting off the unit-norm sublattice preserves the determinant.

theorem TauCeti.IntegralLattice.IsPosDef.isUnimodular_unitNormComplement_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : L.unitNormComplement.IsUnimodular ↔ L.IsUnimodular

The complement of the unit-norm sublattice is unimodular exactly when the lattice is.

theorem TauCeti.IntegralLattice.IsPosDef.finrank_unitNormSubmodule_add_finrank_unitNormComplement {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : Module.finrank ℤ ↥L.unitNormSubmodule + Module.finrank ℤ ↥L.unitNormComplement.carrier = Module.finrank ℤ ↥L.carrier

The ranks of the unit-norm sublattice and of its complement add up to the rank of the lattice.

theorem TauCeti.IntegralLattice.IsPosDef.unitNormSubmodule_eq_top_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : L.unitNormSubmodule = ⊤ ↔ Subsingleton ↥L.unitNormComplement.carrier

A positive definite lattice is spanned by its vectors of norm one exactly when the complement of the unit-norm sublattice is zero.

theorem TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_unitLattice_of_unitNormSubmodule_eq_top {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (htop : L.unitNormSubmodule = ⊤) : Nonempty ((unitLattice (Fin (Module.finrank ℤ ↥L.carrier))).Isometry L)

A positive definite lattice spanned by its vectors of norm one is the standard lattice I_n, with n its rank.

Uniqueness of the splitting

theorem TauCeti.IntegralLattice.Isometry.map_unitNormSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {W : Type v} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) : Submodule.map (↑e.carrierEquiv) L.unitNormSubmodule = M.unitNormSubmodule

An isometry carries the unit-norm sublattice onto the unit-norm sublattice.

theorem TauCeti.IntegralLattice.Isometry.map_orthogonal_unitNormSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {W : Type v} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) : Submodule.map (↑e.carrierEquiv) (L.integralForm.orthogonal L.unitNormSubmodule) = M.integralForm.orthogonal M.unitNormSubmodule

An isometry carries the orthogonal complement of the unit-norm sublattice onto the orthogonal complement of the unit-norm sublattice.

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

Isometric lattices have isometric complements of their unit-norm sublattices.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.coe_unitNormComplementEquiv_symm_unitNormComplement_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {W : Type v} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (e : L.Isometry M) (t : ↥(L.integralForm.orthogonal L.unitNormSubmodule)) : ↑(M.unitNormComplementEquiv.symm (e.unitNormComplement.carrierEquiv (L.unitNormComplementEquiv t))) = e.carrierEquiv ↑t

The isometry Isometry.unitNormComplement acts on the orthogonal complement of the unit-norm sublattice as the carrier equivalence of the original isometry.

noncomputable def TauCeti.IntegralLattice.unitNormComplementOrthogonalSumIsometry {ι : Type u_1} [Fintype ι] {W : Type v} [AddCommGroup W] [Module ℚ W] {N : IntegralLattice W} (hN : N.IsPosDef) (hN1 : N.vectorsOfNorm 1 = ∅) : N.Isometry ((unitLattice ι).orthogonalSum N).unitNormComplement

The complement of the unit-norm sublattice of I_ι ⊕ N is N, when N is positive definite without vectors of norm one.

@[simp]

theorem TauCeti.IntegralLattice.coe_unitNormComplementEquiv_symm_unitNormComplementOrthogonalSumIsometry_apply {ι : Type u_1} [Fintype ι] {W : Type v} [AddCommGroup W] [Module ℚ W] {N : IntegralLattice W} (hN : N.IsPosDef) (hN1 : N.vectorsOfNorm 1 = ∅) (x : ↥N.carrier) : ↑(((unitLattice ι).orthogonalSum N).unitNormComplementEquiv.symm ((unitNormComplementOrthogonalSumIsometry hN hN1).carrierEquiv x)) = ((unitLattice ι).orthogonalSumInr N) x

The isometry unitNormComplementOrthogonalSumIsometry is the second inclusion of I_ι ⊕ N, read in the orthogonal complement of the unit-norm sublattice.

theorem TauCeti.IntegralLattice.nonempty_isometry_of_isometry_orthogonalSum_unitLattice {ι : Type u_1} [Fintype ι] {W : Type v} [AddCommGroup W] [Module ℚ W] {N : IntegralLattice W} {κ : Type u_2} [Fintype κ] {X : Type u_3} [AddCommGroup X] [Module ℚ X] {N' : IntegralLattice X} (hN : N.IsPosDef) (hN1 : N.vectorsOfNorm 1 = ∅) (hN' : N'.IsPosDef) (hN1' : N'.vectorsOfNorm 1 = ∅) (e : ((unitLattice ι).orthogonalSum N).Isometry ((unitLattice κ).orthogonalSum N')) : Nonempty (N.Isometry N')

Cancellation of standard summands. If I_ι ⊕ N ≅ I_κ ⊕ N', where N and N' are positive definite without vectors of norm one, then N ≅ N'.

theorem TauCeti.IntegralLattice.card_eq_of_isometry_orthogonalSum_unitLattice {ι : Type u_1} [Fintype ι] {W : Type v} [AddCommGroup W] [Module ℚ W] {N : IntegralLattice W} {κ : Type u_2} [Fintype κ] {X : Type u_3} [AddCommGroup X] [Module ℚ X] {N' : IntegralLattice X} (hN : N.IsPosDef) (hN1 : N.vectorsOfNorm 1 = ∅) (hN' : N'.IsPosDef) (hN1' : N'.vectorsOfNorm 1 = ∅) (e : ((unitLattice ι).orthogonalSum N).Isometry ((unitLattice κ).orthogonalSum N')) : Fintype.card ι = Fintype.card κ

Cancellation of standard summands, rank part. If I_ι ⊕ N ≅ I_κ ⊕ N', where N and N' are positive definite without vectors of norm one, then #ι = #κ.