The covolume of an integral lattice realized in Euclidean space

A realization of an integral lattice L in a real inner product space E is a ℤ-linear map φ : L → E carrying the integral form to the inner product, ⟪φ x, φ y⟫ = β(x, y), whose image spans E over ℝ. When L is nondegenerate, this file proves that the image φ(L) is a ℤ-lattice in E (discrete and of full rank) and that its covolume, for the volume measure of the inner product, satisfies

covolume(φ(L))² = det L, equivalently covolume(φ(L)) = √(disc L).

This reconciles the analytic covolume of Mathlib's ZLattice with the algebraic determinant of the lattice. The form of a realized lattice is the pullback of an inner product, so only positive semidefinite lattices have realizations, and nondegeneracy is the hypothesis that rules out a collapsing φ: the zero form on ℤ, realized by the zero map into the zero space, has determinant 0 but covolume 1.

Conversely every positive semidefinite lattice of rank n has a map to Euclidean space ℝⁿ carrying its form to the inner product: diagonalize the rational form in an orthogonal basis and rescale the coordinates by the square roots of its nonnegative diagonal values. For a positive definite lattice the image spans, so every positive definite lattice has a realization; this is what lets geometry-of-numbers arguments in ℝⁿ be applied to an abstract positive definite lattice. In particular the determinant of a positive definite lattice is the square of a covolume, hence positive, and a positive definite unimodular lattice has determinant 1.

Main results

• TauCeti.IntegralLattice.gram_comp_eq_map_gramMatrix: the Gram matrix of the image of a carrier basis is the integral Gram matrix of the lattice.
• TauCeti.IntegralLattice.injective_of_inner_eq: a realization of a nondegenerate lattice is injective.
• TauCeti.IntegralLattice.linearIndependent_comp_basis: it carries carrier bases to ℝ-linearly independent families.
• TauCeti.IntegralLattice.discreteTopology_range: the image of a map carrying the integral form to the inner product is discrete; for a full realization it is a ℤ-lattice in E.
• TauCeti.IntegralLattice.covolume_range_sq_eq_determinant: covolume(φ(L))² = det L.
• TauCeti.IntegralLattice.covolume_range_eq_sqrt_discriminant: covolume(φ(L)) = √(disc L).
• TauCeti.IntegralLattice.IsPosSemidef.exists_inner_eq: a positive semidefinite lattice maps to ℝⁿ with its form carried to the inner product.
• TauCeti.IntegralLattice.IsPosDef.exists_realization: a positive definite lattice has a realization in ℝⁿ.
• TauCeti.IntegralLattice.IsPosDef.determinant_pos: a positive definite lattice has positive determinant.
• TauCeti.IntegralLattice.IsPosDef.determinant_eq_one_of_isUnimodular: a positive definite unimodular lattice has determinant 1.

References

• J. W. S. Cassels, An Introduction to the Geometry of Numbers, Chapter I, §2.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 1, §1.

theorem TauCeti.IntegralLattice.gram_comp_eq_map_gramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : ↥L.carrier →ₗ[ℤ] E} (hφ : ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)) {ι : Type u_2} (e : Module.Basis ι ℤ ↥L.carrier) : (Matrix.gram ℝ fun (i : ι) => φ (e i)) = (L.gramMatrix e).map Int.cast

A map carrying the integral form to the inner product carries the integral Gram matrix of a carrier basis to the real Gram matrix of its image.

theorem TauCeti.IntegralLattice.det_gram_comp_eq_determinant {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : ↥L.carrier →ₗ[ℤ] E} (hφ : ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)) {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : (Matrix.gram ℝ fun (i : ι) => φ (e i)).det = ↑L.determinant

A map carrying the integral form to the inner product carries every carrier basis to a family whose Gram determinant is the determinant of the lattice.

theorem TauCeti.IntegralLattice.discreteTopology_range {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : ↥L.carrier →ₗ[ℤ] E} (hφ : ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)) : DiscreteTopology ↥φ.range

The image of a map carrying the integral form to the inner product is discrete: it is an integral lattice.

theorem TauCeti.IntegralLattice.injective_of_inner_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : ↥L.carrier →ₗ[ℤ] E} (hφ : ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)) [L.IsNondegenerate] : Function.Injective ⇑φ

A map carrying the form of a nondegenerate lattice to the inner product is injective.

theorem TauCeti.IntegralLattice.linearIndependent_comp_basis {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : ↥L.carrier →ₗ[ℤ] E} (hφ : ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)) [L.IsNondegenerate] {ι : Type u_2} (e : Module.Basis ι ℤ ↥L.carrier) : LinearIndependent ℝ fun (i : ι) => φ (e i)

A map carrying the form of a nondegenerate lattice to the inner product carries every carrier basis to an ℝ-linearly independent family.

theorem TauCeti.IntegralLattice.covolume_range_sq_eq_determinant {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : ↥L.carrier →ₗ[ℤ] E} (hφ : ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)) [L.IsNondegenerate] (hspan : Submodule.span ℝ (Set.range ⇑φ) = ⊤) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : ZLattice.covolume φ.range MeasureTheory.volume ^ 2 = ↑L.determinant

The covolume identity. The square of the covolume of a nondegenerate integral lattice, realized in a real inner product space, is its determinant.

theorem TauCeti.IntegralLattice.covolume_range_eq_sqrt_discriminant {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {φ : ↥L.carrier →ₗ[ℤ] E} (hφ : ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)) [L.IsNondegenerate] (hspan : Submodule.span ℝ (Set.range ⇑φ) = ⊤) [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : ZLattice.covolume φ.range MeasureTheory.volume = √↑L.discriminant

The covolume of a nondegenerate integral lattice, realized in a real inner product space, is the square root of its discriminant.

Existence of realizations

theorem TauCeti.IntegralLattice.IsPosSemidef.exists_inner_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) : ∃ (φ : ↥L.carrier →ₗ[ℤ] EuclideanSpace ℝ (Fin (Module.finrank ℤ ↥L.carrier))), ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)

A positive semidefinite lattice maps to Euclidean space by its form. A positive semidefinite integral lattice of rank n has a ℤ-linear map to ℝⁿ carrying its integral form to the inner product. In an orthogonal basis of the rational form the map sends a vector to its coordinates, rescaled by the square roots of the nonnegative diagonal values.

theorem TauCeti.IntegralLattice.IsPosDef.exists_realization {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : ∃ (φ : ↥L.carrier →ₗ[ℤ] EuclideanSpace ℝ (Fin (Module.finrank ℤ ↥L.carrier))), (∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)) ∧ Submodule.span ℝ (Set.range ⇑φ) = ⊤

A positive definite lattice has a realization. A positive definite integral lattice of rank n has a ℤ-linear map to ℝⁿ carrying its integral form to the inner product, whose image spans ℝⁿ.

theorem TauCeti.IntegralLattice.IsPosDef.determinant_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : 0 < L.determinant

A positive definite lattice has positive determinant, the square of the covolume of any of its realizations.

theorem TauCeti.IntegralLattice.IsPosDef.determinant_eq_one_of_isUnimodular {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hLp : L.IsPosDef) (hLu : L.IsUnimodular) : L.determinant = 1

A positive definite unimodular lattice has determinant 1.