The lattice of integral points of a rational subspace, and its covolume

For a subspace V ⊆ ℚ^ι the integral points V ∩ ℤ^ι form a lattice of rank dim V in the real span of V, and its covolume is the Arakelov height of V:

covolume (V ∩ ℤ^ι)  =  H_Ar V.

This is the ℚ case of the covolume identity of Layer 4.3 — W. M. Schmidt's H'(S) = H(S) — which over a number field K reads covol (V ∩ 𝓞_K^ι) = 2^{-r₂ k} |discr K|^{k/2} H_Ar(V)^d. Over ℚ the degree d, the discriminant and the number r₂ of complex places are all 1, 1 and 0, so the three constants vanish and the identity is the bare statement above. It is what converts the lattice statement of Minkowski's second theorem (Layer 4.2) into a height statement, and it is the only ingredient Siegel's lemma over ℚ takes from this milestone.

Main definitions

• Rat.piIntCast, Rat.piEuclidean: the coordinatewise casts (ι → ℤ) → (ι → ℚ) and (ι → ℚ) → EuclideanSpace ℝ ι. The second is the ℚ case of NumberField.mixedEmbedding.
• Submodule.intPoints: the integral points V ∩ ℤ^ι of a rational subspace, as a ℤ-submodule of ι → ℤ.
• Submodule.realSpan: the real span of a rational subspace, inside EuclideanSpace ℝ ι.
• Submodule.intLattice: the integral points, as a ℤ-lattice inside Submodule.realSpan. This is the object whose covolume the milestone computes.

Main results

• Submodule.covolume_intLattice: the covolume identity, covolume (V ∩ ℤ^ι) = H_Ar V.
• Submodule.covolume_intLattice_span_singleton: its rank-one case — the covolume of the lattice cut out by a line is the Arakelov height of any rational point spanning it, hence the euclidean norm of the primitive integer point on it.
• Submodule.exists_basis_intPoints: the integral points are free of rank dim V, with a basis that spans V over ℚ and generates all of V ∩ ℤ^ι — the saturation that makes the height come out right.
• Submodule.gcd_plucker_eq_one: the Plücker point of such a basis is a primitive integer vector: the maximal minors of a saturated integral basis are coprime.
• NumberField.arakelovMulHeight_intCast_of_gcd_eq_one: over ℚ, the Arakelov height of a tuple of coprime integers is its euclidean norm. This is the Arakelov analogue of Mathlib's Rat.mulHeight_eq_max_abs_of_gcd_eq_one, which Mathlib states for the sup norm only.
• Submodule.finrank_realSpan, Submodule.mem_intLattice, and the DiscreteTopology and IsZLattice instances that make the covolume meaningful.

Implementation notes

⚠ Both sides of the identity are computed against the same sum of squares of maximal minors, and that is the whole proof. With y a saturated integral basis and p its tuple of Plücker coordinates, ZLattice.covolume_sq_eq_det_gram and the Cauchy–Binet identity of Layer 3.4 give covolume² = det (Y Yᵀ) = ∑ₛ p ₛ², while the height is ∑ₛ p ₛ² under a square root because the finite places contribute 1 — which is exactly the primitivity of p. Neither computation knows about the other; the identity is the statement that the archimedean factor of the height is a Gram determinant and its finite factor is a saturation condition.

⚠ Saturation is not a convenience, it is the content. For an arbitrary ℤ-basis of a finite-index sublattice of V ∩ ℤ^ι the covolume is larger by the index, while the height does not change: the Plücker coordinates are multiplied by the index and the extra factor is cancelled by the finite places. Submodule.gcd_plucker_eq_one is where saturation is spent, and it is spent exactly once.

⚠ The primitivity proof needs no adapted basis, no Smith normal form and no splitting of the quotient. If a prime q divided every maximal minor of y, then the reductions of the y i would be linearly dependent over ZMod q — this is exteriorPower.plucker_eq_zero_iff of Layer 3.1, read over a finite field — so some integral combination ∑ cᵢ yᵢ with a coefficient prime to q would be divisible by q; its quotient by q is an integral point of V, hence a ℤ-combination of the y i by saturation, and independence then forces q ∣ cᵢ for every i. Cassels' Lemma 2 is not on this path either, just as it was not on the path of Layer 4.2.

⚠ The lattice lives in a subspace, and that is why the ambient space is EuclideanSpace. A sublattice of ℤ^ι of rank k < #ι has no covolume in ℝ^ι; the covolume it has is the one measured inside its own real span, and a subspace of a real vector space carries a canonical measure only when the space carries an inner product. Submodule.realSpan is therefore a submodule of EuclideanSpace ℝ ι rather than of ι → ℝ, and ZLattice.covolume is taken against the MeasureSpace instance that Mathlib.MeasureTheory.Measure.Haar.OfBasis puts on any finite-dimensional real inner product space.

⚠ Only the ℚ case is here. The number-field case of Layer 4.3 is Schmidt 1967, §3, Theorem 1, whose two halves — a Lagrange expansion in blocks of d rows for the archimedean factor, and a local counting lemma for [σ(Λ) : Λ₀] = N(𝔞) at the finite places — are not reproduced here. What the ℚ case already settles is the shape of the statement and its normalization: the Arakelov height, not the sup-norm height, is what a covolume equals.

References

W. M. Schmidt, "On heights of algebraic subspaces and diophantine approximations", Annals of Mathematics 85 (1967), 430–472, §3, Theorem 1: H'(S) = H(S), of which the statement here is the case K = ℚ. His Lemma 4 is the archimedean half — over ℚ it is the Cauchy–Binet identity alone — and his Lemmas 5 and 6 the finite half, which over ℚ is the primitivity of the Plücker point.

I. Aliev and M. Henk, "Minkowski's successive minima in convex and discrete geometry", Communications in Mathematics 31(2) (2023), 35–59, §6 (arXiv:2304.00120; doi:10.46298/cm.11155). The rational covolume identity is stated immediately before Theorem 6.3 and used in the geometry-of-numbers proof of Siegel's lemma.

This is Layer 4.3 of the ArithmeticHeights roadmap, over ℚ.

The two coordinatewise casts

def Rat.piIntCast (ι : Type u_1) : (ι → ℤ) →ₗ[ℤ] ι → ℚ

Coordinatewise ℤ → ℚ on tuples, as a ℤ-linear map.

Equations

• Rat.piIntCast ι = { toFun := fun (z : ι → ℤ) (i : ι) => ↑(z i), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Rat.piIntCast_apply {ι : Type u_1} (z : ι → ℤ) (i : ι) : (piIntCast ι) z i = ↑(z i)

theorem Rat.piIntCast_injective {ι : Type u_1} : Function.Injective ⇑(piIntCast ι)

def Rat.piEuclidean (ι : Type u_1) : (ι → ℚ) →ₗ[ℚ] EuclideanSpace ℝ ι

Coordinatewise ℚ → ℝ on tuples, landing in EuclideanSpace ℝ ι, as a ℚ-linear map. This is the ℚ case of NumberField.mixedEmbedding: there are no complex places and the one real place is the inclusion.

Equations

• Rat.piEuclidean ι = { toFun := fun (x : ι → ℚ) => WithLp.toLp 2 fun (i : ι) => ↑(x i), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Rat.piEuclidean_apply {ι : Type u_1} (x : ι → ℚ) (i : ι) : ((piEuclidean ι) x).ofLp i = ↑(x i)

The integral points of a rational subspace

def Submodule.intPoints {ι : Type u_1} (V : Submodule ℚ (ι → ℚ)) : Submodule ℤ (ι → ℤ)

The integral points V ∩ ℤ^ι of a rational subspace, as a ℤ-submodule of ι → ℤ.

Equations

• V.intPoints = Submodule.comap (Rat.piIntCast ι) (Submodule.restrictScalars ℤ V)

@[simp]

theorem Submodule.mem_intPoints {ι : Type u_1} {V : Submodule ℚ (ι → ℚ)} {z : ι → ℤ} : z ∈ V.intPoints ↔ (Rat.piIntCast ι) z ∈ V

instance instFiniteIntSubtypeForallMemSubmoduleIntPoints {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) : Module.Finite ℤ ↥V.intPoints

instance instFreeIntSubtypeForallMemSubmoduleIntPoints {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) : Module.Free ℤ ↥V.intPoints

theorem Submodule.exists_basis_intPoints {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) {k : ℕ} (hV : Module.finrank ℚ ↥V = k) : ∃ (y : Fin k → ι → ℤ), (LinearIndependent ℚ fun (i : Fin k) => (Rat.piIntCast ι) (y i)) ∧ span ℚ (Set.range fun (i : Fin k) => (Rat.piIntCast ι) (y i)) = V ∧ span ℤ (Set.range y) = V.intPoints

A saturated integral basis exists. The integral points of a rational subspace of dimension k are a free ℤ-module of rank k, and a basis of them spans V over ℚ while generating every integral point of V. Both halves are needed: the first makes the basis a basis of the real span, the second is what makes its Plücker point primitive.

Primitivity of the Plücker point

theorem Submodule.gcd_plucker_eq_one {ι : Type u_1} [Fintype ι] [LinearOrder ι] (V : Submodule ℚ (ι → ℚ)) {k : ℕ} {y : Fin k → ι → ℤ} (hy : LinearIndependent ℚ fun (i : Fin k) => (Rat.piIntCast ι) (y i)) (hspan : span ℚ (Set.range fun (i : Fin k) => (Rat.piIntCast ι) (y i)) = V) (hsat : span ℤ (Set.range y) = V.intPoints) : Finset.univ.gcd (exteriorPower.plucker k y) = 1

The maximal minors of a saturated integral basis are coprime. Equivalently: the Plücker point of a rational subspace has a primitive integer representative, namely the one a basis of V ∩ ℤ^ι produces. This is the finite half of the covolume identity — Schmidt's Lemmas 5 and 6 over ℚ — and it is the only place the saturation hypothesis is used.

The real span and the lattice inside it

def Submodule.realSpan {ι : Type u_1} (V : Submodule ℚ (ι → ℚ)) : Submodule ℝ (EuclideanSpace ℝ ι)

The real span of a rational subspace, inside EuclideanSpace ℝ ι.

Equations

• V.realSpan = Submodule.span ℝ (⇑(Rat.piEuclidean ι) '' ↑V)

noncomputable def Submodule.intLattice {ι : Type u_1} (V : Submodule ℚ (ι → ℚ)) : Submodule ℤ ↥V.realSpan

The integral points of V as a lattice in its real span: the object whose covolume is the Arakelov height of V.

Equations

• V.intLattice = Submodule.comap (↑ℤ V.realSpan.subtype) (Submodule.map (↑ℤ (Rat.piEuclidean ι) ∘ₗ Rat.piIntCast ι) V.intPoints)

theorem Submodule.mem_intLattice {ι : Type u_1} {V : Submodule ℚ (ι → ℚ)} {w : ↥V.realSpan} : w ∈ V.intLattice ↔ ∃ (z : ι → ℤ), (Rat.piIntCast ι) z ∈ V ∧ ↑w = (Rat.piEuclidean ι) ((Rat.piIntCast ι) z)

instance instDiscreteTopologySubtypeEuclideanSpaceRealMemSubmoduleRealSpanIntIntLattice {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) : DiscreteTopology ↥V.intLattice

theorem Submodule.finrank_realSpan {ι : Type u_1} [Finite ι] (V : Submodule ℚ (ι → ℚ)) : Module.finrank ℝ ↥V.realSpan = Module.finrank ℚ ↥V

The real span of a rational subspace has the dimension of the subspace.

instance instIsZLatticeRealSubtypeEuclideanSpaceMemSubmoduleRealSpanIntLattice {ι : Type u_1} [Fintype ι] (V : Submodule ℚ (ι → ℚ)) : IsZLattice ℝ V.intLattice

The Arakelov height of a primitive integer tuple

theorem NumberField.arakelovMulHeight_intCast_of_gcd_eq_one {κ : Type u_1} [Fintype κ] {x : κ → ℤ} (hx : Finset.univ.gcd x = 1) : arakelovMulHeight (Int.cast ∘ x) = √(∑ i : κ, ↑(x i) ^ 2)

Over ℚ the Arakelov height of a tuple of coprime integers is its euclidean norm. The finite places contribute 1 — this is Mathlib's Rat.iSup_finitePlace_apply_eq_one_of_gcd_eq_one — and the single infinite place is real, so the archimedean factor is the ℓ² norm with exponent 1. Mathlib's Rat.mulHeight_eq_max_abs_of_gcd_eq_one is the same statement for the sup norm.

The covolume identity

theorem Submodule.covolume_intLattice {ι : Type u_1} [Fintype ι] [LinearOrder ι] (V : Submodule ℚ (ι → ℚ)) : ZLattice.covolume V.intLattice MeasureTheory.volume = V.arakelovMulHeight

The covolume identity over ℚ (Layer 4.3, the case K = ℚ; W. M. Schmidt 1967, §3, Theorem 1). The lattice of integral points of a rational subspace has covolume the Arakelov height of the subspace.

theorem Submodule.covolume_intLattice_span_singleton {ι : Type u_1} [Fintype ι] [LinearOrder ι] {x : ι → ℚ} (hx : x ≠ 0) : ZLattice.covolume (ℚ ∙ x).intLattice MeasureTheory.volume = NumberField.arakelovMulHeight x

The rank-one case. The lattice cut out by the line through a nonzero rational point has covolume the Arakelov height of that point — for a primitive integer point, its euclidean norm.