Plücker coordinates

For a family x : Fin p → ι → R of p vectors with coordinates in a linearly ordered type ι, its Plücker coordinates are its maximal minors: for each p-element subset s of ι, the determinant of the p × p matrix whose rows are the vectors x i restricted to the coordinates in s, listed in increasing order. The subsets are indexed by Mathlib's Set.powersetCard ι p, the index type of the induced basis of the exterior power.

The coordinates are those of the exterior product x 0 ∧ ⋯ ∧ x (p - 1) in the basis of ⋀[R]^p (ι → R) induced by the standard basis. Consequently a change of the family by a square matrix multiplies all coordinates by its determinant, and over an integral domain they vanish identically exactly when the family is linearly dependent. Plücker coordinates give the point in projective space attached to a subspace of K^ι, and heights of subspaces are heights of these points.

The Cauchy–Binet formula expresses the determinant of the p × p product of two such families as the sum of products of their Plücker coordinates. Over a commutative star ring, for instance ℂ, applying it to a family and its conjugate writes the Hermitian Gram determinant of the family as the sum of the squared absolute values of its Plücker coordinates.

Over a field, the Plücker coordinates of complementary orthogonal families are complementary minors: if x and y are linearly independent families of p and q vectors with p + q = #ι, and every x i has dot product zero with every y j, then, up to a common nonzero factor and signs, the coordinate of y at a q-element subset t is the coordinate of x at the complement of t. This is what makes the height of a subspace equal to the height of its orthogonal complement.

The determinant identities hold over an arbitrary commutative ring. The comparison with linear independence holds over an integral domain and the complementary minors over a field, while the coprimality theorem for saturated submodules holds over a principal ideal domain with a normalized gcd. The empty family has a single Plücker coordinate, equal to 1, and a family of more than #ι vectors has none.

Main definitions

• TauCeti.plucker x: the Plücker coordinates of a family x : Fin p → ι → R.

Main results

• TauCeti.plucker_eq_repr_ιMulti: the Plücker coordinates are the coordinates of exteriorPower.ιMulti R p x in the exterior-power basis induced by Pi.basisFun R ι.
• TauCeti.plucker_sum_smul: replacing the family by its product with a square matrix multiplies the Plücker coordinates by the determinant of that matrix.
• TauCeti.det_mul_transpose_eq_sum_plucker_mul: the Cauchy–Binet formula.
• Matrix.det_mul_transpose_eq_sum_plucker_sq: its Gram-determinant form for a matrix.
• Matrix.det_mul_transpose_nonneg and Matrix.det_mul_transpose_pos_iff: over a commutative ring with a compatible linear order, the Gram determinant of a matrix is nonnegative; over a linearly ordered commutative ring, it is positive exactly when the rows are linearly independent.
• TauCeti.det_mul_conjTranspose_eq_sum_plucker_mul_star: its Hermitian form.
• TauCeti.plucker_ne_zero_iff: over an integral domain, the Plücker coordinates of a family are not all zero exactly when the family is linearly independent.
• TauCeti.exists_plucker_eq_mul_plucker_compl_or_eq_neg: the Plücker coordinates of complementary orthogonal families are complementary minors, up to a common nonzero factor and signs.
• TauCeti.gcd_plucker_eq_one: the Plücker coordinates of a basis of a saturated submodule of R^ι over a principal ideal domain are coprime.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §2.8.
• J.-H. Evertse and R. G. Ferretti, A further improvement of the quantitative Subspace Theorem, Ann. of Math. 177 (2013), §6.1, (6.13).

The proofs use Mathlib's exterior-power basis Module.Basis.exteriorPower and its coordinate formula exteriorPower.ιMultiDual_apply_ιMulti, by Sophie Morel and Daniel Morrison. The statement of TauCeti.gcd_plucker_eq_one is adapted from Ralf Stephan's Submodule.gcd_plucker_eq_one in ArithmeticHeights/RationalLattice.lean of rwst/Subspace-Theorems, commit 9894a1c4baf805296b249e95575f0e16e8e1afa3 (Apache 2.0); the proof here instead uses a projection onto the saturated submodule and the Cauchy–Binet formula, so it works over any principal ideal domain with a normalized gcd.

def TauCeti.plucker {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p : ℕ} (x : Fin p → ι → R) (s : ↑(Set.powersetCard ι p)) : R

The Plücker coordinates of a family x of p vectors in ι → R: at a p-element subset s of ι, the p × p minor of the matrix with rows x i on the columns in s, taken in increasing order.

theorem TauCeti.plucker_apply {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p : ℕ} (x : Fin p → ι → R) (s : ↑(Set.powersetCard ι p)) : plucker x s = (Matrix.of fun (i j : Fin p) => x i ((Set.powersetCard.ofFinEmbEquiv.symm s) j)).det

The Plücker coordinate at s is the minor on the columns in s.

theorem Matrix.exists_det_submatrix_eq_sign_mul_plucker {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p : ℕ} (A : Matrix (Fin p) ι R) (e : Fin p ↪ ι) : ∃ (σ : Equiv.Perm (Fin p)), (A.submatrix id ⇑e).det = ↑↑(Equiv.Perm.sign σ) * TauCeti.plucker A.row (Set.powersetCard.ofFinEmb p ι e)

A maximal minor on any enumeration of its columns is the Plücker coordinate on its sorted range, multiplied by a permutation sign.

@[simp]

theorem TauCeti.plucker_of_isEmpty {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] (x : Fin 0 → ι → R) (s : ↑(Set.powersetCard ι 0)) : plucker x s = 1

The empty family has Plücker coordinate 1.

@[simp]

theorem TauCeti.plucker_ofSingleton {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] (x : Fin 1 → ι → R) (i : ι) : plucker x (Set.powersetCard.ofSingleton i) = x 0 i

The Plücker coordinate of a single vector at the singleton {i} is its i-th coordinate.

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

Plücker coordinates commute with ring homomorphisms applied to all coordinates.

theorem Matrix.plucker_row_map {R : Type u_1} {S : Type u_2} {ι : Type u_3} [CommRing R] [CommRing S] [LinearOrder ι] {p : ℕ} (f : R →+* S) (A : Matrix (Fin p) ι R) : TauCeti.plucker (A.map ⇑f).row = ⇑f ∘ TauCeti.plucker A.row

The maximal minors of a matrix with a ring homomorphism applied to all entries are the images of the maximal minors of the matrix.

theorem TauCeti.plucker_sum_smul {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p : ℕ} (A : Matrix (Fin p) (Fin p) R) (x : Fin p → ι → R) (s : ↑(Set.powersetCard ι p)) : plucker (fun (i : Fin p) => ∑ k : Fin p, A i k • x k) s = A.det * plucker x s

Replacing a family by its product with a square matrix A multiplies its Plücker coordinates by det A.

theorem Matrix.plucker_append_mul {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p q : ℕ} (A : Matrix (Fin p) (Fin p) R) (B : Matrix (Fin q) (Fin q) R) (x : Matrix (Fin p) ι R) (y : Matrix (Fin q) ι R) (s : ↑(Set.powersetCard ι (p + q))) : TauCeti.plucker (Fin.append (A * x).row (B * y).row) s = A.det * B.det * TauCeti.plucker (Fin.append x.row y.row) s

Applying row operations separately to two concatenated families scales their maximal minors by the product of the two determinants.

theorem Matrix.plucker_append_sub_mul {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p q : ℕ} (x : Matrix (Fin p) ι R) (y : Matrix (Fin q) ι R) (C : Matrix (Fin q) (Fin p) R) (s : ↑(Set.powersetCard ι (p + q))) : TauCeti.plucker (Fin.append x.row (y - C * x).row) s = TauCeti.plucker (Fin.append x.row y.row) s

Subtracting combinations of a first row block from a second block leaves all maximal minors of their concatenation unchanged.

theorem TauCeti.plucker_eq_repr_ιMulti {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p : ℕ} [Finite ι] (x : Fin p → ι → R) (s : ↑(Set.powersetCard ι p)) : plucker x s = ((Module.Basis.exteriorPower p (Pi.basisFun R ι)).repr ((exteriorPower.ιMulti R p) x)) s

The Plücker coordinates of x are the coordinates of the exterior product of x in the basis of ⋀[R]^p (ι → R) induced by the standard basis of ι → R.

theorem TauCeti.det_mul_transpose_eq_sum_plucker_mul {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p : ℕ} [Fintype ι] (x y : Fin p → ι → R) : (Matrix.of x * (Matrix.of y).transpose).det = ∑ s : ↑(Set.powersetCard ι p), plucker x s * plucker y s

The Cauchy–Binet formula. The determinant of the p × p matrix of pairwise products ∑ₖ x i k * y j k is the sum over the p-element subsets s of ι of the products of the Plücker coordinates of x and y at s. For p > #ι both sides vanish.

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

The Cauchy–Binet formula for a Gram determinant. The determinant of A Aᵀ is the sum of the squares of the maximal minors of A, the Plücker coordinates of its rows.

theorem Matrix.det_mul_transpose_nonneg {R : Type u_4} {m : Type u_5} {n : Type u_6} [CommRing R] [LinearOrder R] [IsOrderedRing R] [Fintype m] [DecidableEq m] [Fintype n] (A : Matrix m n R) : 0 ≤ (A * A.transpose).det

Over a commutative ring with a compatible linear order, the Gram determinant det (A * Aᵀ) of the rows of a matrix is nonnegative: by the Cauchy–Binet formula it is a sum of squares.

theorem Matrix.det_mul_transpose_pos_iff {R : Type u_4} {m : Type u_5} {n : Type u_6} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m n R} : 0 < (A * A.transpose).det ↔ LinearIndependent R A.row

Over a linearly ordered commutative ring, the Gram determinant det (A * Aᵀ) of the rows of a matrix is positive exactly when the rows are linearly independent.

theorem TauCeti.det_mul_conjTranspose_eq_sum_plucker_mul_star {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p : ℕ} [StarRing R] [Fintype ι] (x : Fin p → ι → R) : (Matrix.of x * (Matrix.of x).conjTranspose).det = ∑ s : ↑(Set.powersetCard ι p), plucker x s * star (plucker x s)

The Cauchy–Binet formula, Hermitian form. Over a commutative star ring, the determinant of the Hermitian Gram matrix ∑ₖ x i k * star (x j k) of a family is the sum of the products of its Plücker coordinates with their conjugates.

theorem TauCeti.plucker_ne_zero_iff {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p : ℕ} [IsDomain R] [Finite ι] (x : Fin p → ι → R) : plucker x ≠ 0 ↔ LinearIndependent R x

Over an integral domain, the Plücker coordinates of a family are not all zero exactly when it is linearly independent.

Complementary minors

theorem TauCeti.exists_plucker_eq_mul_plucker_compl_or_eq_neg {ι : Type u_3} [LinearOrder ι] {p : ℕ} {K : Type u_4} [Field K] [Fintype ι] {q : ℕ} (hm : p + q = Fintype.card ι) {x : Fin p → ι → K} {y : Fin q → ι → K} (hx : LinearIndependent K x) (hy : LinearIndependent K y) (hxy : ∀ (i : Fin p) (j : Fin q), x i ⬝ᵥ y j = 0) : ∃ (c : K), c ≠ 0 ∧ ∀ (t : ↑(Set.powersetCard ι q)), plucker y t = c * plucker x ((Set.powersetCard.compl hm) t) ∨ plucker y t = -(c * plucker x ((Set.powersetCard.compl hm) t))

Complementary minors. Let x and y be linearly independent families of p and q vectors in K^ι, with p + q = #ι, such that every x i has dot product zero with every y j; so y is a basis of the orthogonal complement of the span of x. Then, up to a common nonzero factor c and signs, the Plücker coordinate of y at a q-element subset t of ι is the Plücker coordinate of x at the complement of t.

theorem TauCeti.gcd_plucker_eq_one {R : Type u_1} {ι : Type u_3} [CommRing R] [LinearOrder ι] {p : ℕ} [IsDomain R] [IsPrincipalIdealRing R] [NormalizedGCDMonoid R] [Fintype ι] {N : Submodule R (ι → R)} (hN : ∀ (c : R) (z : ι → R), c ≠ 0 → c • z ∈ N → z ∈ N) (b : Module.Basis (Fin p) R ↥N) : Finset.univ.gcd (plucker fun (i : Fin p) => ↑(b i)) = 1

The Plücker coordinates of a saturated basis over a PID are coprime. Let N be a saturated submodule of R^ι: it contains every z of which it contains a nonzero multiple. Then the Plücker coordinates of any basis of N have normalized greatest common divisor 1.