The height of the row space and the kernel of an integer matrix

Let A be a p × ι integer matrix and let g = Matrix.minorGcd A be the greatest common divisor of its maximal minors, equivalently of the Plücker coordinates TauCeti.plucker A.row of its rows (Matrix.minorGcd_eq_gcd_plucker). The absolute Euclidean height of the rational row space of A, and that of the rational solution space of A y = 0, satisfy g · subspaceHeight (ker A) = √det (A Aᵀ), which holds without any rank hypothesis: if the rows of A are linearly dependent, then all maximal minors vanish and both sides are zero. If the rows of A are linearly independent, then g ≠ 0 and both heights are √det (A Aᵀ) / g.

With Submodule.covolume_intLattice this computes the covolume of the lattice of integral solutions of A y = 0: for A with linearly independent rows it is √det (A Aᵀ) / g. This is the quantity bounding the product of the sup norms of independent integral solutions in Bombieri and Vaaler's version of Siegel's lemma, and the identity shows that it is unchanged when A is replaced by any integer matrix with the same rational row space.

Main results

• Matrix.minorGcd_mul_subspaceHeight_span_range_row: the identity for the row space.
• Matrix.minorGcd_mul_subspaceHeight_ker_mulVecLin: the identity for the kernel.
• Matrix.covolume_intLattice_ker_mulVecLin: the covolume of the lattice of integral solutions.
• Matrix.sqrt_det_div_minorGcd_mul_left and Matrix.sqrt_det_div_minorGcd_unit_mul: the quotient √det (A Aᵀ) / g is unchanged by A ↦ B * A for det B ≠ 0, in particular for B ∈ GL_m(ℤ), unlike Siegel's bound in terms of the entries of A. This is proved directly, without a rank hypothesis: the maximal minors are multiplied by det B and the Gram determinant by det B ^ 2.

Implementation notes

The height of the row space is the Euclidean height of the Plücker coordinates of the rows (Submodule.subspaceHeight_span_range). Dividing out the greatest common divisor (TauCeti.gcd_mul_height2_intCast) leaves the Euclidean norm of the maximal minors, whose square is det (A Aᵀ) by the Cauchy–Binet formula (TauCeti.det_mul_transpose_eq_sum_plucker_mul). The kernel is the orthogonal complement of the row space for the dot product (Matrix.checkedBy_eq_euclideanDual_generatedBy), which has the same height (Submodule.subspaceHeight_euclideanDual).

References

• E. Bombieri and J. Vaaler, On Siegel's lemma, Invent. Math. 73 (1983), 11–32, Theorem 2.
• I. Aliev and M. Henk, Minkowski's successive minima in convex and discrete geometry, Commun. Math. 31 (2023), no. 2, 35–59, §6.

The proof plan follows Ralf Stephan's Int.Matrix.minorGcd_mul_arakelovMulHeight_ker and NumberField.gcd_mul_arakelovMulHeight_intCast in ArithmeticHeights/BombieriVaaler.lean of rwst/Subspace-Theorems, commit 09835cb23557ae5ae0cf55a9c4ab9055f5d60338 (Apache 2.0).

theorem Matrix.minorGcd_mul_subspaceHeight_span_range_row {ι : Type u_1} [Fintype ι] [LinearOrder ι] {p : ℕ} (A : Matrix (Fin p) ι ℤ) : ↑A.minorGcd * (Submodule.span ℚ (Set.range (A.map Int.cast).row)).subspaceHeight = √↑(A * A.transpose).det

The height of the row space of an integer matrix. The greatest common divisor of the maximal minors of an integer matrix A, times the absolute Euclidean height of the rational row space of A, is √det (A Aᵀ). If the rows are linearly dependent, both sides vanish.

theorem Matrix.minorGcd_mul_subspaceHeight_ker_mulVecLin {ι : Type u_1} [Fintype ι] [LinearOrder ι] {p : ℕ} (A : Matrix (Fin p) ι ℤ) : ↑A.minorGcd * (A.map Int.cast).mulVecLin.ker.subspaceHeight = √↑(A * A.transpose).det

The height of the kernel of an integer matrix. The greatest common divisor of the maximal minors of an integer matrix A, times the absolute Euclidean height of the space of rational solutions of A y = 0, is √det (A Aᵀ). If the rows are linearly dependent, both sides vanish.

theorem Matrix.covolume_intLattice_ker_mulVecLin {ι : Type u_1} [Fintype ι] [LinearOrder ι] {p : ℕ} {A : Matrix (Fin p) ι ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row) : ZLattice.covolume (A.map Int.cast).mulVecLin.ker.intLattice MeasureTheory.volume = √↑(A * A.transpose).det / ↑A.minorGcd

The covolume of the lattice of integral solutions of A y = 0. For an integer matrix A with linearly independent rows, the lattice of integral solutions of A y = 0 has covolume √det (A Aᵀ) divided by the greatest common divisor of the maximal minors of A.

theorem Matrix.sqrt_det_div_minorGcd_mul_left {m : Type u_2} {n : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] {B : Matrix m m ℤ} (hB : B.det ≠ 0) (A : Matrix m n ℤ) : √↑(B * A * (B * A).transpose).det / ↑(B * A).minorGcd = √↑(A * A.transpose).det / ↑A.minorGcd

The quotient √det (A * Aᵀ) / minorGcd A is unchanged by A ↦ B * A for any square integer matrix B with det B ≠ 0: both numerator and denominator are multiplied by |det B|.

theorem Matrix.sqrt_det_div_minorGcd_unit_mul {m : Type u_2} {n : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] (U : GL m ℤ) (A : Matrix m n ℤ) : √↑(↑U * A * (↑U * A).transpose).det / ↑(↑U * A).minorGcd = √↑(A * A.transpose).det / ↑A.minorGcd

The quotient √det (A * Aᵀ) / minorGcd A is invariant under A ↦ U * A for U ∈ GL_m(ℤ).