Finitely many classes of positive definite integral forms

For every rank n and every bound D, there is a finite set of integral n × n matrices containing a Gram matrix of every symmetric positive definite ℤ-valued bilinear form on a free ℤ-module of rank n whose Gram determinant is at most D. In other words, positive definite integral forms of given rank and bounded determinant fall into finitely many isometry classes.

The proof is Hermite's reduction, by induction on the rank. Let v be a vector of least norm μ = B(v, v). It is primitive, and Hermite's inequality bounds μ by the determinant. On a complement of ℤ v the condensed form

S(y, z) = μ · B(y, z) - B(y, v) · B(v, z)

is positive definite of rank n - 1, its determinant is bounded by Chiò's identity, and it does not change when multiples of v are added to y and z. By induction, S has a Gram matrix H in a finite set. Adding to each vector of the corresponding basis a multiple of v brings B(v, ·) to values r in [0, μ), and then the Gram matrix of B in the basis v, y₁, …, y_{n-1} is determined by μ, r and H: its lower block is (H + r rᵀ) / μ.

The argument is specific to definite forms: for an indefinite form there is no vector of least norm, and the corresponding finiteness theorem needs a different proof.

Main results

• LinearMap.BilinForm.exists_finset_forall_exists_toMatrix_mem: positive definite integral forms of rank n and determinant at most D have Gram matrices in a fixed finite set.

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 LinearMap.BilinForm.exists_finset_forall_exists_toMatrix_mem (n : ℕ) (D : ℤ) : ∃ (S : Finset (Matrix (Fin n) (Fin n) ℤ)), ∀ {M : Type u} [inst : AddCommGroup M] (B : LinearMap.BilinForm ℤ M), B.IsSymm → (BilinMap.toQuadraticMap B).PosDef → ∀ (b : Module.Basis (Fin n) ℤ M), ((toMatrix b) B).det ≤ D → ∃ (c : Module.Basis (Fin n) ℤ M), (toMatrix c) B ∈ S

Finiteness of classes of positive definite integral forms. For every rank n and bound D there is a finite set S of integral matrices such that every symmetric positive definite ℤ-valued bilinear form B on a free ℤ-module of rank n, with Gram determinant at most D, has a Gram matrix in S. Hence there are only finitely many isometry classes of such forms.