Modified for Lean/Mathlib 4.35.0: add the explicit inner-product Haar-measure import.

The covolume of a lattice as a Gram determinant

For a ℤ-lattice L in a finite-dimensional real inner product space, the covolume of L — the volume of a fundamental domain for the canonical measure, the one giving the parallelepiped of an orthonormal basis volume 1 — is the square root of the Gram determinant det ⟪b i, b j⟫ of any ℤ-basis b of L.

This is the form in which a covolume is computed in the geometry of numbers whenever the lattice is presented by generators rather than by a fundamental domain, and it is the step that turns the covolume of a lattice of rational points into a sum of squares of maximal minors: composed with the Cauchy–Binet identity it says that the squared covolume of the lattice spanned by the rows of a matrix is the sum of the squares of its maximal minors.

Mathlib has ZLattice.covolume_eq_det, the corresponding statement in ι → ℝ with the Lebesgue measure, where the answer is the determinant of the basis matrix; in an inner product space there is no ambient basis to take a determinant against, and the Gram matrix is what replaces it.

Main results

• ZLattice.covolume_eq_abs_det_orthonormalBasis: the covolume is the absolute determinant of the coordinate matrix of a ℤ-basis in any orthonormal basis of the ambient space.
• ZLattice.covolume_sq_eq_det_gram: the squared covolume is the Gram determinant of any ℤ-basis.
• ZLattice.covolume_eq_sqrt_det_gram: the covolume is the square root of that determinant.

Implementation notes

Mathlib's naming convention in Mathlib/Algebra/Module/ZLattice/Covolume.lean is that a result about ι → ℝ carries the plain name and its InnerProductSpace counterpart carries a prime. The three results here are not primed counterparts of anything: covolume_eq_det has no Gram matrix in it, and the Gram determinant is not available in ι → ℝ without choosing an inner product.

The index type of the ℤ-basis is arbitrary; the orthonormal basis of the ambient space is obtained from stdOrthonormalBasis by reindexing along the equivalence that ZLattice.rank— through Basis.ofZLatticeBasis — provides, so no hypothesis relating the index type to Module.finrank is needed.

References

J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer (1959), Chapter I, §2.1, pp. 9–10, defines the lattice determinant as the absolute determinant of a basis matrix. The Gram formula proved here is the corresponding Euclidean computation for a lattice in a subspace, using orthonormal coordinates on its span.

This is Layer 4.3 of the ArithmeticHeights roadmap, the infrastructure half: the covolume identity of that milestone is proved by computing both sides of it against a Gram determinant.

theorem ZLattice.covolume_eq_abs_det_orthonormalBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {κ : Type u_2} [Fintype κ] [DecidableEq κ] (b : Module.Basis κ ℤ ↥L) (o : OrthonormalBasis κ ℝ E) : covolume L MeasureTheory.volume = |(o.toBasis.toMatrix (Subtype.val ∘ ⇑b)).det|

The covolume against an orthonormal basis. The parallelepiped of an orthonormal basis has volume 1, so the covolume of a lattice is the absolute determinant of the coordinates of any of its ℤ-bases in any orthonormal basis of the ambient space.

theorem ZLattice.covolume_sq_eq_det_gram {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {κ : Type u_2} [Fintype κ] [DecidableEq κ] (b : Module.Basis κ ℤ ↥L) : covolume L MeasureTheory.volume ^ 2 = (Matrix.of fun (i j : κ) => inner ℝ ↑(b i) ↑(b j)).det

The squared covolume is the Gram determinant of any ℤ-basis.

theorem ZLattice.covolume_eq_sqrt_det_gram {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] {κ : Type u_2} [Fintype κ] [DecidableEq κ] (b : Module.Basis κ ℤ ↥L) : covolume L MeasureTheory.volume = √(Matrix.of fun (i j : κ) => inner ℝ ↑(b i) ↑(b j)).det

The covolume is the square root of the Gram determinant of any ℤ-basis.

theorem ZLattice.det_gram_of_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {κ : Type u_2} [Fintype κ] [DecidableEq κ] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : E →ₗ[ℝ] F) (A : E →ₗ[ℝ] E) (b : Module.Basis κ ℝ E) (h : ∀ (x y : E), inner ℝ (f x) (f y) = inner ℝ (A x) y) : (Matrix.of fun (i j : κ) => inner ℝ (f (b i)) (f (b j))).det = LinearMap.det A * (Matrix.of fun (i j : κ) => inner ℝ (b i) (b j)).det

A linear map multiplies a Gram determinant by the determinant of its Gram operator. If A satisfies ⟪f x, f y⟫ = ⟪A x, y⟫ — that is, A = f* f — then the Gram matrix of the image of a basis is Mᵀ G, with G the Gram matrix of the basis and M the matrix of A. This is the linear-algebra form of the statement that a linear map scales volume by √(det (f* f)), which is the factor by which it scales a covolume.

theorem ZLattice.det_gram_comp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {κ : Type u_2} [Fintype κ] [DecidableEq κ] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (f : E →ₗ[ℝ] F) (b : Module.Basis κ ℝ E) : (Matrix.of fun (i j : κ) => inner ℝ (f (b i)) (f (b j))).det = LinearMap.det (LinearMap.adjoint f ∘ₗ f) * (Matrix.of fun (i j : κ) => inner ℝ (b i) (b j)).det

The adjoint form of ZLattice.det_gram_of_inner.

theorem ZLattice.covolume_sq_eq_det_gram_comp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {κ : Type u_2} [Fintype κ] [DecidableEq κ] {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F] {W : Submodule ℝ F} (L : Submodule ℤ ↥W) [DiscreteTopology ↥L] [IsZLattice ℝ L] (c : Module.Basis κ ℤ ↥L) (f : E →ₗ[ℝ] F) (A : E →ₗ[ℝ] E) (b : Module.Basis κ ℝ E) (h : ∀ (x y : E), inner ℝ (f x) (f y) = inner ℝ (A x) y) (hc : ∀ (i : κ), ↑↑(c i) = f (b i)) : covolume L MeasureTheory.volume ^ 2 = LinearMap.det A * (Matrix.of fun (i j : κ) => inner ℝ (b i) (b j)).det

The covolume of the image of a lattice under a linear map. If a ℤ-basis of a lattice sitting in a subspace W of F is the image under f of an ℝ-basis b, then its squared covolume is det A times the Gram determinant of b, for any A with ⟪f x, f y⟫ = ⟪A x, y⟫. This is the form in which the archimedean half of a covolume identity is computed: the lattice is transported from a space where its covolume is known, and the transport factor is an operator determinant.