Maximal minors and their gcd

A maximal minor of a matrix A with rows indexed by m and columns indexed by n is the determinant det (A.submatrix id e) of the square submatrix on all the rows and on the columns picked out by an embedding e : m ↪ n. Over an integral domain the rows of A are linearly independent exactly when some maximal minor is nonzero, by the criterion in TauCeti.LinearAlgebra.Matrix.Rank. That module also proves invariance of row independence under scalar extension between domains.

Over a GCD domain, Matrix.minorGcd A is the normalized gcd of the maximal minors. Left multiplication by a square matrix B multiplies every maximal minor by det B, so it multiplies the minor gcd by normalize (det B) and leaves it unchanged for B invertible. For an integer matrix A with linearly independent rows, the quotient √det (A * Aᵀ) / minorGcd A is the covolume of the lattice of integer solutions of A *ᵥ x = 0, which enters the sharp form of Siegel's lemma due to Bombieri and Vaaler; that quotient and its invariance under A ↦ B * A are treated in TauCeti.NumberTheory.Height.Arakelov.IntMatrix. The examples at the end of the file compute the minor gcd and Gram determinant of the row [2, 2] and of a matrix after a unimodular shear; the matrix before the shear is treated in TauCeti.Examples.NumberTheory.Height.Arakelov.BombieriVaaler.

The Gram determinant det (A * Aᵀ) is mostly treated elsewhere: its behaviour under A ↦ B * A and its independence criterion are in TauCeti.LinearAlgebra.Matrix.Gram, and its positivity, a consequence of the Cauchy–Binet formula, is in TauCeti.LinearAlgebra.ExteriorPower.Plucker. Only its integer case under independence over ℚ, Matrix.det_mul_transpose_pos, is stated here, next to the matching Matrix.one_le_minorGcd.

Main definitions

• Matrix.minorGcd: the normalized gcd of the maximal minors.

Main results

• Matrix.minorGcd_ne_zero_iff: the minor gcd is nonzero exactly when the rows are linearly independent.
• Matrix.minorGcd_mul_left and Matrix.minorGcd_unit_mul: left multiplication by B multiplies the minor gcd by normalize (det B), and leaves it unchanged for B invertible.
• Matrix.minorGcd_eq_gcd_plucker: the minor gcd is the gcd of the Plücker coordinates TauCeti.plucker A.row of the rows.
• Matrix.one_le_minorGcd and Matrix.det_mul_transpose_pos: the minor gcd of an integer matrix is at least 1 and its Gram determinant is positive when its rows are linearly independent over ℚ.

References

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

theorem Matrix.det_submatrix_mul_left {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [CommRing R] (B : Matrix m m R) (A : Matrix m n R) (e : m → n) : ((B * A).submatrix id e).det = B.det * (A.submatrix id e).det

A minor of B * A on all the rows is det B times the corresponding minor of A.

noncomputable def Matrix.minorGcd {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [CommRing R] [NormalizedGCDMonoid R] (A : Matrix m n R) : R

The gcd of the maximal minors of A: the normalized gcd of the determinants det (A.submatrix id e) over all embeddings e : m ↪ n. It is 0 exactly when every maximal minor vanishes, in particular when n has fewer elements than m.

theorem Matrix.minorGcd_def {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [CommRing R] [NormalizedGCDMonoid R] (A : Matrix m n R) : A.minorGcd = Finset.univ.gcd fun (e : m ↪ n) => (A.submatrix id ⇑e).det

theorem Matrix.minorGcd_dvd {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [CommRing R] [NormalizedGCDMonoid R] (A : Matrix m n R) (e : m ↪ n) : A.minorGcd ∣ (A.submatrix id ⇑e).det

theorem Matrix.dvd_minorGcd_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [CommRing R] [NormalizedGCDMonoid R] {A : Matrix m n R} {a : R} : a ∣ A.minorGcd ↔ ∀ (e : m ↪ n), a ∣ (A.submatrix id ⇑e).det

@[simp]

theorem Matrix.normalize_minorGcd {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [CommRing R] [NormalizedGCDMonoid R] (A : Matrix m n R) : normalize A.minorGcd = A.minorGcd

theorem Matrix.minorGcd_eq_zero_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [CommRing R] [NormalizedGCDMonoid R] {A : Matrix m n R} : A.minorGcd = 0 ↔ ∀ (e : m ↪ n), (A.submatrix id ⇑e).det = 0

theorem Matrix.minorGcd_ne_zero_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [CommRing R] [NormalizedGCDMonoid R] [Nontrivial R] {A : Matrix m n R} : A.minorGcd ≠ 0 ↔ LinearIndependent R A.row

The minor gcd is nonzero exactly when the rows are linearly independent.

@[simp]

theorem Matrix.minorGcd_unit_mul {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [CommRing R] [NormalizedGCDMonoid R] (U : GL m R) (A : Matrix m n R) : (↑U * A).minorGcd = A.minorGcd

Left multiplication by an invertible matrix does not change the minor gcd.

theorem Matrix.minorGcd_mul_left {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [DecidableEq m] [Fintype n] [CommRing R] [StrongNormalizedGCDMonoid R] (B : Matrix m m R) (A : Matrix m n R) : (B * A).minorGcd = normalize B.det * A.minorGcd

Left multiplication by B multiplies the minor gcd by normalize (det B).

theorem Matrix.minorGcd_eq_gcd_plucker {R : Type u_3} {ι : Type u_4} [Fintype ι] [LinearOrder ι] {p : ℕ} [CommRing R] [NormalizedGCDMonoid R] (A : Matrix (Fin p) ι R) : A.minorGcd = Finset.univ.gcd (TauCeti.plucker A.row)

For a matrix with rows indexed by Fin p and linearly ordered columns, the minor gcd is the gcd of the Plücker coordinates of the rows: these are the maximal minors on columns taken in increasing order, and every maximal minor is one of them up to sign.

theorem Matrix.minorGcd_nonneg {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] (A : Matrix m n ℤ) : 0 ≤ A.minorGcd

theorem Matrix.minorGcd_pos_iff {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m n ℤ} : 0 < A.minorGcd ↔ LinearIndependent ℤ A.row

The minor gcd of an integer matrix is positive exactly when its rows are linearly independent.

theorem Matrix.one_le_minorGcd {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m n ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row) : 1 ≤ A.minorGcd

The minor gcd of an integer matrix whose rows are linearly independent over ℚ is at least 1.

theorem Matrix.det_mul_transpose_pos {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m n ℤ} (hA : LinearIndependent ℚ (A.map Int.cast).row) : 0 < (A * A.transpose).det

The Gram determinant of an integer matrix whose rows are linearly independent over ℚ is positive.

Examples