The covolume of the lattice of integral points of a rational subspace #
For a subspace V of ℚ^ι, the covolume of the lattice V ∩ ℤ^ι in the real span of V
(Submodule.intLattice) is the absolute Euclidean height of V:
covolume (V ∩ ℤ^ι) = subspaceHeight V.
This is the identity through which theorems of the geometry of numbers about the lattice
V ∩ ℤ^ι, such as Minkowski's theorems, become statements about the height of V. It is the
case K = ℚ of Schmidt's identity between the covolume of the lattice V ∩ 𝓞_K^ι and the height
of a subspace V of K^ι, which over a general number field also involves the discriminant and
the complex places of K.
The lattice is the whole intersection V ∩ ℤ^ι, which is saturated in ℤ^ι. The covolume of a
sublattice of finite index is larger by the index, while the height of V does not change.
Main results #
Submodule.covolume_intLattice: the covolume ofV.intLatticeisV.subspaceHeight.
Implementation notes #
Both sides of the identity are computed from the Plücker coordinates p of a ℤ-basis of
V ∩ ℤ^ι. The squared covolume is the Gram determinant of the basis
(ZLattice.covolume_sq_eq_det_gram), which is ∑ s, p s ^ 2 by the Cauchy–Binet formula. The
height is √(∑ s, p s ^ 2): saturation makes p primitive (TauCeti.gcd_plucker_eq_one), so the
finite places contribute nothing (TauCeti.height2_intCast_eq_sqrt_of_gcd_eq_one).
References #
- W. M. Schmidt, On heights of algebraic subspaces and diophantine approximations, Ann. of Math. 85 (1967), 430–472, §3, Theorem 1.
- E. Bombieri and J. Vaaler, On Siegel's lemma, Invent. Math. 73 (1983), 11–32.
The proof plan is adapted from Ralf Stephan's ArithmeticHeights/RationalLattice.lean in
rwst/Subspace-Theorems,
commit 9894a1c4baf805296b249e95575f0e16e8e1afa3 (Apache 2.0).
The covolume of the lattice of integral points of a rational subspace is its absolute
Euclidean height. For a subspace V of ℚ^ι, the lattice V ∩ ℤ^ι in the real span of V
has covolume V.subspaceHeight.