The Cauchy–Binet identity

The product of a matrix with the transpose of another is a determinant that the maximal minors compute: det (A Bᵀ) = ∑ₛ det Aₛ · det Bₛ, the sum over the sets s of m columns. Taking B = A turns the sum of squares of the maximal minors into the Gram determinant det (A Aᵀ) of the rows, and taking B = conj A turns the sum of their squared absolute values into det (A Aᴴ). Those two are the archimedean local factors of the Arakelov height of the tuple of minors — of the row space, by Layer 3.3 — and they are where the √|det (A Aᵀ)| of the Bombieri–Vaaler bound comes from.

Everything here is proved once, over an arbitrary commutative ring, for the Plücker coordinates of Layer 3.1; the matrix statements are that identity read through Layer 3.3's dictionary.

Main results

• exteriorPower.sum_plucker_mul_plucker: the identity itself, for two families of vectors — ∑ₛ plucker k v s * plucker k w s is the determinant of the matrix of dot products v i ⬝ᵥ w j.
• Matrix.det_mul_eq_sum_plucker and Matrix.det_mul_transpose_eq_sum_plucker, with Matrix.det_mul_eq_sum_det_submatrix and Matrix.det_mul_transpose_eq_sum_det_submatrix spelling the same statements with Matrix.submatrix and Finset.orderEmbOfFin.
• Matrix.det_mul_transpose_self_eq_sum_sq: the real specialization, det (A Aᵀ) is the sum of the squares of the maximal minors, over any commutative ring.
• Matrix.det_mul_conjTranspose_self_eq_sum: the complex specialization, over a commutative star ring, with Matrix.det_mul_conjTranspose_self_eq_sum_sq_norm its RCLike form det (A Aᴴ) = ∑ₛ ‖det Aₛ‖² and NumberField.InfinitePlace.det_map_embedding_mul_conjTranspose_self its form at an infinite place of a number field, which is the local factor named above.
• Matrix.det_mul_transpose_self_eq_zero_iff and Matrix.linearIndependent_row_iff_det_mul_transpose_self_ne_zero: over an ordered field the Gram determinant of the rows detects full row rank, the Gram criterion.
• exteriorPower.plucker_map: the Plücker coordinates commute with a ring homomorphism, which is what carries the identity to a completion or an embedding.

Implementation notes

The proof is Mathlib's pairing exteriorPower.pairingDual between ⋀ⁿ (Dual R M) and ⋀ⁿ M, evaluated on the image of a wedge under exteriorPower.map n (Pi.basisFun R ι).toDual. Read on the induced basis of the exterior power that composite is the diagonal bilinear form ∑ₛ xₛ yₛ, because Basis.toDual sends the standard basis to the dual basis and exteriorPower.ιMultiDual — the coordinate functional of Layer 3.1's basis — is by definition the pairing against the wedge of dual basis vectors; read on wedges it is a determinant of dot products, by exteriorPower.pairingDual_ιMulti_ιMulti. So the identity is the statement that one bilinear form has two descriptions, and no expansion of a determinant over permutations is carried out anywhere.

Mathlib's LinearMap.BilinForm.exteriorPower is that same composite and would be the natural name for it. What is missing is its defining equation: LinearMap.BilinForm.bilinForm_ιMulti_ιMulti, which evaluates the form on two wedges as a determinant, carries no public in a module that has no public section, so it is invisible outside its own file and every user has to re-prove it. That proof is exactly the content of the identity below, so the composite is written out here.

Pi.basisFun_toDual_apply, that Basis.toDual of the standard basis is the dot product, is stated here because Mathlib has Basis.toDual_apply_left only for a basis vector in the second argument.

References

A. L. Cauchy (1812) and J. P. M. Binet (1812); the identity is Proposition 2.8.8 of E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), and §2 Lemma 1 of W. M. Schmidt, "On heights of algebraic subspaces and diophantine approximations", Annals of Mathematics 85 (1967), 430–472. It enters the Siegel-lemma literature as the local-height formula (iv) in §2, p. 15, of E. Bombieri and J. Vaaler, "On Siegel's lemma", Inventiones Mathematicae 73 (1983), 11–32, whose bound is stated in terms of √|det (A Aᵀ)|.

This is Layer 3.4 of the ArithmeticHeights roadmap.

The identity in Plücker coordinates

theorem Pi.basisFun_toDual_apply {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (x y : ι → R) : ((basisFun R ι).toDual x) y = x ⬝ᵥ y

The dual map of the standard basis is the dot product. Mathlib's Basis.toDual_apply_left evaluates b.toDual x on a basis vector; for the standard basis of ι → R the value on an arbitrary vector is the dot product.

theorem exteriorPower.sum_plucker_mul_plucker {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (k : ℕ) (v w : Fin k → ι → R) : ∑ s : ↑(Set.powersetCard ι k), plucker k v s * plucker k w s = (Matrix.of fun (i j : Fin k) => v i ⬝ᵥ w j).det

The Cauchy–Binet identity. The sum over the k-element sets of columns of the product of the two Plücker coordinates is the determinant of the k × k matrix of dot products. Over any commutative ring, and with no hypothesis on either family.

theorem exteriorPower.plucker_map {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {S : Type u_3} [CommRing S] (f : R →+* S) (k : ℕ) (v : Fin k → ι → R) (s : ↑(Set.powersetCard ι k)) : plucker k (fun (i : Fin k) => ⇑f ∘ v i) s = f (plucker k v s)

The Plücker coordinates commute with a ring homomorphism, each being a determinant. This is what carries the identity along an embedding of a number field into ℂ.

The identity for matrices

theorem Matrix.plucker_row_map {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} {S : Type u_3} [CommRing S] (f : R →+* S) (A : Matrix (Fin m) ι R) (s : ↑(Set.powersetCard ι m)) : exteriorPower.plucker m (A.map ⇑f).row s = f (exteriorPower.plucker m A.row s)

The Plücker coordinates of the rows commute with a ring homomorphism applied entrywise.

theorem Matrix.det_mul_transpose_eq_sum_plucker {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} (A B : Matrix (Fin m) ι R) : (A * B.transpose).det = ∑ s : ↑(Set.powersetCard ι m), exteriorPower.plucker m A.row s * exteriorPower.plucker m B.row s

The Cauchy–Binet identity, for A Bᵀ: the determinant of the matrix of dot products of the rows of A with the rows of B is the sum over the sets of m columns of the products of corresponding maximal minors.

theorem Matrix.det_mul_eq_sum_plucker {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι R) (B : Matrix ι (Fin m) R) : (A * B).det = ∑ s : ↑(Set.powersetCard ι m), exteriorPower.plucker m A.row s * exteriorPower.plucker m B.col s

The Cauchy–Binet identity, for a product A B of an m × ι by an ι × m matrix: the determinant is the sum over the sets of m indices of the product of the maximal minor of A on those columns with the maximal minor of B on those rows.

theorem Matrix.det_mul_transpose_eq_sum_det_submatrix {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} (A B : Matrix (Fin m) ι R) : (A * B.transpose).det = ∑ s : ↑(Set.powersetCard ι m), (A.submatrix id ⇑((↑s).orderEmbOfFin ⋯)).det * (B.submatrix id ⇑((↑s).orderEmbOfFin ⋯)).det

The Cauchy–Binet identity in the submatrix spelling of Layer 3.3: the minors are taken on the columns of s, enumerated in increasing order.

theorem Matrix.det_mul_eq_sum_det_submatrix {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι R) (B : Matrix ι (Fin m) R) : (A * B).det = ∑ s : ↑(Set.powersetCard ι m), (A.submatrix id ⇑((↑s).orderEmbOfFin ⋯)).det * (B.submatrix (⇑((↑s).orderEmbOfFin ⋯)) id).det

The Cauchy–Binet identity for A B in the submatrix spelling: the maximal minors of A on the columns of s against those of B on the rows of s.

The Gram determinant of the rows

theorem Matrix.det_mul_transpose_self_eq_sum_sq {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι R) : (A * A.transpose).det = ∑ s : ↑(Set.powersetCard ι m), exteriorPower.plucker m A.row s ^ 2

The archimedean specialization at a real place. The Gram determinant of the rows is the sum of the squares of the maximal minors. This is the √|det (A Aᵀ)| of the Bombieri–Vaaler bound: its square is the ℓ² local factor of the tuple of minors.

theorem Matrix.det_mul_transpose_self_nonneg {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} {S : Type u_3} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] (A : Matrix (Fin m) ι S) : 0 ≤ (A * A.transpose).det

The Gram determinant of the rows is nonnegative.

theorem Matrix.det_mul_transpose_self_eq_zero_iff {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (A : Matrix (Fin m) ι K) : (A * A.transpose).det = 0 ↔ ¬LinearIndependent K A.row

The Gram criterion. Over an ordered field the Gram determinant of the rows vanishes exactly when the rows are linearly dependent.

theorem Matrix.det_mul_transpose_self_pos_iff {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (A : Matrix (Fin m) ι K) : 0 < (A * A.transpose).det ↔ LinearIndependent K A.row

The Gram criterion, in the form the Bombieri–Vaaler bound needs: full row rank is exactly positivity of the Gram determinant, so √|det (A Aᵀ)| is nonzero there.

theorem Matrix.linearIndependent_row_iff_det_mul_transpose_self_ne_zero {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} {K : Type u_4} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (A : Matrix (Fin m) ι K) : LinearIndependent K A.row ↔ (A * A.transpose).det ≠ 0

Full row rank, detected by the Gram determinant.

The Gram determinant at a complex place

theorem Matrix.det_mul_conjTranspose_self_eq_sum {R : Type u_1} [CommRing R] [StarRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} (A : Matrix (Fin m) ι R) : (A * A.conjTranspose).det = ∑ s : ↑(Set.powersetCard ι m), exteriorPower.plucker m A.row s * star (exteriorPower.plucker m A.row s)

The archimedean specialization at a complex place. Pairing A against its conjugate transpose replaces the squares of the maximal minors by their norms.

theorem Matrix.det_mul_conjTranspose_self_eq_sum_sq_norm {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} {K : Type u_3} [RCLike K] (A : Matrix (Fin m) ι K) : (A * A.conjTranspose).det = ↑(∑ s : ↑(Set.powersetCard ι m), ‖exteriorPower.plucker m A.row s‖ ^ 2)

The complex specialization, with the squared absolute values displayed: det (A Aᴴ) is the square of the ℓ² norm of the tuple of maximal minors.

theorem NumberField.InfinitePlace.det_map_embedding_mul_conjTranspose_self {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {m : ℕ} (v : InfinitePlace K) (A : Matrix (Fin m) ι K) : (A.map ⇑v.embedding * (A.map ⇑v.embedding).conjTranspose).det = ↑(∑ s : ↑(Set.powersetCard ι m), v (exteriorPower.plucker m A.row s) ^ 2)

The archimedean local factor of the tuple of maximal minors is a Gram determinant. At an infinite place v of a number field, ∑ₛ v(det Aₛ)² — the quantity the ℓ² normalization of Layer 0.1 raises to the power mult v / 2 — is the determinant of the Gram matrix of the rows of A read through the embedding attached to v. At a real place the conjugate transpose is the transpose, so this covers both kinds of place.