Finitely many classes of positive definite lattices

There are only finitely many isometry classes of positive definite integral lattices of a given rank and bounded determinant. This is the positive definite case of the finiteness of the class number; definiteness is essential to the proof, which is Hermite's reduction (LinearMap.BilinForm.exists_finset_forall_exists_toMatrix_mem).

The statement takes two forms. First, a single finite set of integral matrices contains a Gram matrix of every such lattice, whatever its ambient rational space. Second, since lattices with bases of equal Gram matrices are isometric (TauCeti.IntegralLattice.Isometry.ofGramMatrixEq), a family of pairwise non-isometric such lattices is finite.

Main results

• TauCeti.IntegralLattice.exists_finset_forall_exists_gramMatrix_mem: a finite set of matrices containing a Gram matrix of every positive definite lattice of rank n and determinant at most D.
• TauCeti.IntegralLattice.finite_of_pairwise_isEmpty_isometry: a family of pairwise non-isometric positive definite lattices of rank n and determinant at most D is finite.

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.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 9, §1.

theorem TauCeti.IntegralLattice.exists_finset_forall_exists_gramMatrix_mem (n : ℕ) (D : ℤ) : ∃ (S : Finset (Matrix (Fin n) (Fin n) ℤ)), ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module ℚ V] (L : IntegralLattice V), L.IsPosDef → Module.finrank ℤ ↥L.carrier = n → L.determinant ≤ D → ∃ (b : Module.Basis (Fin n) ℤ ↥L.carrier), L.gramMatrix b ∈ S

Finitely many Gram matrices represent all positive definite lattices of given rank and bounded determinant. For every rank n and bound D there is a finite set S of integral matrices such that every positive definite integral lattice of rank n and determinant at most D, in any rational space, has a Gram matrix in S.

theorem TauCeti.IntegralLattice.finite_of_pairwise_isEmpty_isometry {ι : Type u_1} {V : ι → Type u} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℚ (V i)] (L : (i : ι) → IntegralLattice (V i)) {n : ℕ} {D : ℤ} (hpos : ∀ (i : ι), (L i).IsPosDef) (hrank : ∀ (i : ι), Module.finrank ℤ ↥(L i).carrier = n) (hdet : ∀ (i : ι), (L i).determinant ≤ D) (hL : Pairwise fun (i j : ι) => IsEmpty ((L i).Isometry (L j))) : Finite ι

There are finitely many classes of positive definite lattices of given rank and bounded determinant. A family of pairwise non-isometric positive definite integral lattices of rank n and determinant at most D is finite.