The genus of unimodular lattices

Evenness is a genus invariant (TauCeti.IntegralLattice.SameGenus.isEven_iff), since it is detected by the dyadic localization. For unimodular lattices it is, together with the signature, a complete invariant of the genus: two unimodular lattices lie in one genus exactly when they have the same signature and are both even or both odd.

The determinant of a unimodular lattice is (-1) ^ n₋, so only the prime 2 needs a local comparison. There the unimodular forms over ℤ_[2] are classified by rank, type, determinant square class and oddity, and the oddity of a unimodular lattice is its signature modulo 8 by van der Blij's theorem (TauCeti.IntegralLattice.vanDerBlij). For instance, the odd unimodular lattices of signature (p, q) form the single genus of I_{p,q} = ⟨1⟩ ^ p ⊕ ⟨-1⟩ ^ q.

Main results

• TauCeti.IntegralLattice.sameGenus_iff_of_isUnimodular: unimodular lattices lie in one genus exactly when their signatures agree and they are even together.

References

• J.-P. Serre, A Course in Arithmetic, Chapter V, §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 15, §7.

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

The genus of a unimodular lattice. Two unimodular lattices lie in one genus exactly when their signatures agree and they are both even or both odd.