Positive definite unimodular lattices of rank at most nine

A positive definite unimodular lattice of rank at most nine is the standard lattice Iₙ, the root lattice E₈, or I₁ ⊕ E₈. In particular E₈ is the unique even unimodular positive definite lattice of rank eight.

For a positive definite unimodular lattice L of rank n, Hermite's inequality 3 ^ (n choose 2) · (min L)ⁿ ≤ 4 ^ (n choose 2) bounds the minimum:

• if 1 ≤ n ≤ 5, then min L = 1, since 3 ^ (n choose 2) · 2ⁿ > 4 ^ (n choose 2);
• if n ≤ 8, then min L ≤ 2: in rank zero the minimum is zero, and if 1 ≤ n ≤ 8, then 3 ^ (n choose 2) · 3ⁿ > 4 ^ (n choose 2).

Both ranges are the exact ones in which this inequality excludes the next value of the minimum. Combined with the splitting L ≅ I_k ⊕ L₀ of the vectors of norm one, the first bound shows that a positive definite unimodular lattice of rank at most five is Iₙ; equivalently, a nonzero positive definite unimodular lattice without vectors of norm one has rank at least six.

Hermite's inequality also gives vectors of norm two up to rank nine. Applied to the even sublattice, which has determinant at most four, it shows that a positive definite unimodular lattice of rank between two and nine has a vector r of norm two. Applied to the orthogonal complement of r inside the vectors pairing evenly with r, which has rank n - 1 and determinant two, it gives a second vector s of norm at most two orthogonal to r.

Now let L have no vectors of norm one, so r and s both have norm two. The two-neighbor of L along r + s contains the orthonormal vectors (r + s) / 2 and (r - s) / 2, so it is I_k ⊕ M₀ with k ≥ 2 and M₀ of rank n - k ≤ n - 2 ≤ 7 and without vectors of norm one. In rank at most seven such an M₀ is zero: by induction from rank at most five, since otherwise the neighbor is Iₙ and 4 ∣ n. Hence the neighbor is Iₙ. A two-neighbor of Iₙ without vectors of norm one has 4 ∣ n and, in rank eight, is E₈. So L is zero or E₈, and the classification follows from the splitting L ≅ I_k ⊕ L₀.

Main declarations

• TauCeti.IntegralLattice.IsPosDef.minimum_eq_one_of_isUnimodular: a nonzero lattice of rank at most five has minimum one.
• TauCeti.IntegralLattice.IsPosDef.minimum_le_two_of_isUnimodular: in rank at most eight the minimum is at most two.
• TauCeti.IntegralLattice.IsPosDef.six_le_finrank_of_vectorsOfNorm_one_eq_empty: a nonzero positive definite unimodular lattice without vectors of norm one has rank at least six.
• TauCeti.IntegralLattice.IsPosDef.minimum_eq_two_of_vectorsOfNorm_one_eq_empty and TauCeti.IntegralLattice.IsPosDef.minimum_eq_two_of_isUnimodular_of_isEven: in rank at most eight such a lattice, and in particular a nonzero even unimodular lattice, has minimum two.
• TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_unitLattice_of_isUnimodular: a positive definite unimodular lattice of rank at most five is Iₙ.
• TauCeti.IntegralLattice.IsPosDef.exists_integralNorm_eq_two_of_isUnimodular: in rank between two and nine there is a vector of norm two.
• TauCeti.IntegralLattice.IsPosDef.exists_integralForm_eq_zero_of_integralNorm_eq_two: in rank at most nine a vector of norm two is orthogonal to a nonzero vector of norm at most two.
• TauCeti.IntegralLattice.IsPosDef.subsingleton_of_vectorsOfNorm_one_eq_empty_of_finrank_le_seven: without vectors of norm one, a lattice of rank at most seven is zero.
• IsPosDef.nonempty_isometry_typeE₈RootLattice_of_vectorsOfNorm_one_eq_empty: without vectors of norm one, a nonzero lattice of rank at most nine is E₈.
• TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_of_isUnimodular_of_finrank_le_nine: a lattice of rank at most nine is Iₙ, E₈ or I₁ ⊕ E₈.
• TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_typeE₈RootLattice_of_isEven: an even lattice of rank eight is E₈.

References

• C. Hermite, Extraits de lettres de M. Ch. Hermite à M. Jacobi sur différents objets de la théorie des nombres, J. Reine Angew. Math. 40 (1850), 261–315.
• M. Kneser, Klassenzahlen definiter quadratischer Formen, Arch. Math. 8 (1957), 241--250.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 16.
• O. T. O'Meara, Introduction to Quadratic Forms, §106.

theorem TauCeti.IntegralLattice.IsPosDef.minimum_eq_one_of_isUnimodular {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) [Nontrivial ↥L.carrier] (hn : Module.finrank ℤ ↥L.carrier ≤ 5) : L.minimum = 1

A nonzero positive definite unimodular lattice of rank at most five has minimum one.

theorem TauCeti.IntegralLattice.IsPosDef.minimum_le_two_of_isUnimodular {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) (hn : Module.finrank ℤ ↥L.carrier ≤ 8) : L.minimum ≤ 2

A positive definite unimodular lattice of rank at most eight has minimum at most two.

theorem TauCeti.IntegralLattice.IsPosDef.six_le_finrank_of_vectorsOfNorm_one_eq_empty {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) [Nontrivial ↥L.carrier] (h1 : L.vectorsOfNorm 1 = ∅) : 6 ≤ Module.finrank ℤ ↥L.carrier

A nonzero positive definite unimodular lattice without vectors of norm one has rank at least six.

theorem TauCeti.IntegralLattice.IsPosDef.minimum_eq_two_of_vectorsOfNorm_one_eq_empty {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) [Nontrivial ↥L.carrier] (h1 : L.vectorsOfNorm 1 = ∅) (hn : Module.finrank ℤ ↥L.carrier ≤ 8) : L.minimum = 2

A nonzero positive definite unimodular lattice of rank at most eight without vectors of norm one has minimum two.

theorem TauCeti.IntegralLattice.IsPosDef.minimum_eq_two_of_isUnimodular_of_isEven {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) [Nontrivial ↥L.carrier] (he : L.IsEven) (hn : Module.finrank ℤ ↥L.carrier ≤ 8) : L.minimum = 2

A nonzero even positive definite unimodular lattice of rank at most eight has minimum two.

theorem TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_unitLattice_of_isUnimodular {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) (hn : Module.finrank ℤ ↥L.carrier ≤ 5) : Nonempty ((unitLattice (Fin (Module.finrank ℤ ↥L.carrier))).Isometry L)

A positive definite unimodular lattice of rank at most five is the standard lattice Iₙ.

theorem TauCeti.IntegralLattice.IsPosDef.exists_integralNorm_eq_two_of_isUnimodular {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) (h2 : 2 ≤ Module.finrank ℤ ↥L.carrier) (h9 : Module.finrank ℤ ↥L.carrier ≤ 9) : ∃ (x : ↥L.carrier), L.integralNorm x = 2

A positive definite unimodular lattice of rank between two and nine has a vector of norm two. Such a vector already lies in the even sublattice.

theorem TauCeti.IntegralLattice.IsPosDef.exists_integralForm_eq_zero_of_integralNorm_eq_two {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) (h9 : Module.finrank ℤ ↥L.carrier ≤ 9) {r : ↥L.carrier} (hr : L.integralNorm r = 2) : ∃ (s : ↥L.carrier), s ≠ 0 ∧ (L.integralForm r) s = 0 ∧ L.integralNorm s ≤ 2

In a positive definite unimodular lattice of rank at most nine, every vector of norm two is orthogonal to a nonzero vector of norm at most two.

theorem TauCeti.IntegralLattice.IsPosDef.subsingleton_of_vectorsOfNorm_one_eq_empty_of_finrank_le_seven {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) (h1 : L.vectorsOfNorm 1 = ∅) (hn : Module.finrank ℤ ↥L.carrier ≤ 7) : Subsingleton ↥L.carrier

A positive definite unimodular lattice of rank at most seven without vectors of norm one is zero.

theorem TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_typeE₈RootLattice_of_vectorsOfNorm_one_eq_empty {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) [Nontrivial ↥L.carrier] (h1 : L.vectorsOfNorm 1 = ∅) (hn : Module.finrank ℤ ↥L.carrier ≤ 9) : Nonempty (typeE₈RootLattice.Isometry L)

A nonzero positive definite unimodular lattice of rank at most nine without vectors of norm one is E₈.

theorem TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_of_isUnimodular_of_finrank_le_nine {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) (hn : Module.finrank ℤ ↥L.carrier ≤ 9) : Nonempty ((unitLattice (Fin (Module.finrank ℤ ↥L.carrier))).Isometry L) ∨ Nonempty (typeE₈RootLattice.Isometry L) ∨ Nonempty (((unitLattice (Fin 1)).orthogonalSum typeE₈RootLattice).Isometry L)

Positive definite unimodular lattices of rank at most nine. Such a lattice is the standard lattice Iₙ, the root lattice E₈, or I₁ ⊕ E₈.

theorem TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_typeE₈RootLattice_of_isEven {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (hU : L.IsUnimodular) (he : L.IsEven) (hn : Module.finrank ℤ ↥L.carrier = 8) : Nonempty (typeE₈RootLattice.Isometry L)

E₈ is the unique even unimodular positive definite lattice of rank eight.