The genus of even unimodular lattices

Two even unimodular lattices with equal signatures lie in one genus, by the description of the genus of a unimodular lattice through its signature and type (TauCeti.IntegralLattice.sameGenus_iff_of_isUnimodular). In particular, the positive definite even unimodular lattices of a given rank form a single genus.

From rank sixteen on, this genus has more than one class. For k ≥ 2 the lattices E₈^k and D_{8k}⁺ are both positive definite, even and unimodular of rank 8k, hence in one genus, but they are not isometric: the roots of E₈^k span it, while every root of D_{8k}⁺ lies in the checkerboard sublattice D_{8k}, of index two. At k = 2 this is the pair E₈ ⊕ E₈ and D₁₆⁺. That these two lattices are the only classes of their genus is not proved here. In rank eight the same construction gives no second class: D₈⁺ is isometric to E₈.

Main results

• TauCeti.IntegralLattice.sameGenus_of_isEven_of_isUnimodular: even unimodular lattices with equal signatures lie in one genus.
• TauCeti.IntegralLattice.IsPosDef.sameGenus_of_isEven_of_isUnimodular: positive definite even unimodular lattices of equal rank lie in one genus.
• TauCeti.IntegralLattice.sameGenus_e8PowLattice_checkerboardPlusLattice: E₈^k and D_{8k}⁺ lie in one genus.
• TauCeti.IntegralLattice.isEmpty_isometry_e8PowLattice_checkerboardPlusLattice: for k ≥ 2, E₈^k and D_{8k}⁺ are not isometric.

References

• J.-P. Serre, A Course in Arithmetic, Chapter V, §1.4 and §2.
• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Chapter II.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 16, §1.

theorem TauCeti.IntegralLattice.sameGenus_of_isEven_of_isUnimodular {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (hLe : L.IsEven) (hMe : M.IsEven) (hLu : L.IsUnimodular) (hMu : M.IsUnimodular) (hsig : L.signature = M.signature) : L.SameGenus M

Even unimodular lattices with equal signatures lie in one genus. This is the even case of TauCeti.IntegralLattice.sameGenus_iff_of_isUnimodular.

theorem TauCeti.IntegralLattice.IsPosDef.sameGenus_of_isEven_of_isUnimodular {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (hLp : L.IsPosDef) (hMp : M.IsPosDef) (hLe : L.IsEven) (hMe : M.IsEven) (hLu : L.IsUnimodular) (hMu : M.IsUnimodular) (hrank : Module.finrank ℤ ↥L.carrier = Module.finrank ℤ ↥M.carrier) : L.SameGenus M

Positive definite even unimodular lattices of equal rank lie in one genus.

theorem TauCeti.IntegralLattice.sameGenus_e8PowLattice_checkerboardPlusLattice (k : ℕ) : (e8PowLattice k).SameGenus (checkerboardPlusLattice (8 * k) ⋯)

E₈^k and D_{8k}⁺ lie in one genus: both are positive definite, even and unimodular of rank 8k.

theorem TauCeti.IntegralLattice.isEmpty_isometry_e8PowLattice_checkerboardPlusLattice {k : ℕ} (hk : 2 ≤ k) : IsEmpty ((e8PowLattice k).Isometry (checkerboardPlusLattice (8 * k) ⋯))

E₈^k and D_{8k}⁺ are not isometric for k ≥ 2. The roots of E₈^k span it, while the roots of D_{8k}⁺ span at most D_{8k}. At k = 2 these are the two even unimodular lattices E₈ ⊕ E₈ and D₁₆⁺ of rank sixteen.