The covolume of a lattice in an inner product space

In a finite-dimensional real inner product space, equipped with the volume measure of its inner product, the square of the covolume of a ℤ-lattice is the determinant of the Gram matrix of any of its ℤ-bases. This is the metric form of ZLattice.covolume_eq_det, which computes the covolume in the coordinate space ι → ℝ as the absolute determinant of a basis.

The Gram determinant is computed from inner products alone, so this identity expresses the covolume, a measure-theoretic invariant of the lattice, through the metric data of any of its bases. In particular the covolume does not depend on a choice of coordinates, and two lattices with the same Gram matrix in some bases have the same covolume.

Main results

• ZLattice.covolume_sq_eq_det_gram: covolume L ^ 2 is the determinant of the Gram matrix of any ℤ-basis of L.

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.gram ℝ fun (i : ι) => ↑(b i)).det

The square of the covolume of a lattice in a finite-dimensional real inner product space is the determinant of the Gram matrix of any ℤ-basis of the lattice.