Goal
Define the genus of an integral lattice L (all lattices M on the same quadratic space with M_p ≅ L_p for every prime p, including p = ∞) and its class number (the number of isometry classes in the genus).
What already exists
- mathlib:
ZLattice, quadratic forms, QuadraticForm equivalence/isometry; Localization/Completion machinery.
What's missing
SameGenus L M : Prop via local (p-adic and real) isometry, and classNumber L := #(genus L / isometry) (finite).
Test cases
- Even unimodular lattices: in dim 8 the genus has class number 1 (only
E₈); in dim 16, class number 2 (E₈², D₁₆⁺); in dim 24, 24 (Niemeier).
LMFDB targets
New area, not yet in the Verso blueprint — links go to the LMFDB knowls.
Goal
Define the genus of an integral lattice
L(all latticesMon the same quadratic space withM_p ≅ L_pfor every primep, includingp = ∞) and its class number (the number of isometry classes in the genus).What already exists
ZLattice, quadratic forms,QuadraticFormequivalence/isometry;Localization/Completionmachinery.What's missing
SameGenus L M : Propvia local (p-adic and real) isometry, andclassNumber L := #(genus L / isometry)(finite).Test cases
E₈); in dim 16, class number 2 (E₈²,D₁₆⁺); in dim 24, 24 (Niemeier).LMFDB targets
lattice.genuslattice.class_numberlattice.isometrylattice.unimodularNew area, not yet in the Verso blueprint — links go to the LMFDB knowls.