The Plücker point of a subspace

A k-dimensional subspace V of ι → K determines a point of the projective space on Set.powersetCard ι k → K, the tuple of its Plücker coordinates: wedge a basis of V together inside ⋀[K]^k (ι → K) and read the result in the basis that the standard basis of ι → K induces there. A change of basis of V multiplies the wedge by a determinant, hence by a unit, so the point of projective space depends on V alone.

This file builds that point and proves it is an embedding of the k-dimensional subspaces into projective space. Layer 3.2 defines the height of a subspace as the height of this point, and everything the height inherits — Northcott for subspaces above all — rests on the injectivity proved here.

Main definitions

• exteriorPower.plucker k v for v : Fin k → (ι → K): the coordinate tuple of the wedge v 0 ∧ ⋯ ∧ v (k-1), indexed by the k-element subsets of ι.
• Submodule.pluckerPoint V hV for hV : Module.finrank K V = k: the induced point of Projectivization K (Set.powersetCard ι k → K).

Main results

• exteriorPower.plucker_apply: the Plücker coordinate at s is the maximal minor on the columns s of the matrix whose rows are the v i. exteriorPower.plucker_fin_eq_det is the top-rank case, where the single coordinate is the determinant, and exteriorPower.plucker_one_ofSingleton the rank-one case, where the coordinates are the coordinates of the vector.
• exteriorPower.plucker_eq_zero_iff: the coordinate tuple vanishes exactly when the family is linearly dependent, so a basis of V produces a nonzero tuple.
• Submodule.pluckerPoint_eq_mk and Submodule.pluckerPoint_span_range: the value of the Plücker point on any basis of V, and on any linearly independent family spanning it. This is the basis-independence, stated in the form that is actually used. Submodule.pluckerPoint_span_singleton is the rank-one case: the Plücker point of a line is the point itself.
• Submodule.pluckerPoint_injective: distinct subspaces of the same rank have distinct Plücker points.

Two lemmas are stated here because Mathlib lacks them and the proofs need them: exteriorPower.ιMulti_eq_zero_iff, that over a field a wedge vanishes exactly on linearly dependent families, and linearIndependent_fin1, the Fin 1 companion of Mathlib's linearIndependent_fin2.

Implementation notes

The index type is Mathlib's Set.powersetCard ι k, the type of k-element finsets of ι, because that is what Module.Basis.exteriorPower is indexed by; using it verbatim is what lets exteriorPower.plucker_apply come out of Mathlib's exteriorPower.ιMultiDual_apply_ιMulti with no index bookkeeping of our own. It is also why [LinearOrder ι] is a standing hypothesis: an order on ι is needed to say which wedge of basis vectors a k-element subset names. A different order changes each coordinate by a sign only, so nothing downstream depends on the choice.

The Plücker point is not built by Projectivization.lift. There is no projective space to lift from: the data that varies is a basis of V, and bases do not form a projectivization. What takes its place is Submodule.pluckerPoint_eq_mk, which says the value on an arbitrary basis is the value on the chosen one, and which is the only thing a proof ever needs from well-definedness. The definition itself picks Module.finBasisOfFinrankEq.

Injectivity is proved through the wedge criterion exteriorPower.ιMulti_snoc_eq_zero_iff: a vector lies in the span of a linearly independent family exactly when wedging it on gives 0. Since the wedge of a basis of V is recovered from the Plücker point up to a nonzero scalar, and scaling does not change what the criterion detects, the point determines the subspace. The criterion itself is proved in ExteriorAlgebra K (ι → K), where wedging on is multiplication.

References

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §2.8.4.

M. Hindry and J. H. Silverman, Diophantine Geometry: An Introduction, Springer GTM 201 (2000), Exercise A.1.11(a)–(b).

This is Layer 3.1 of the ArithmeticHeights roadmap.

theorem linearIndependent_fin1 {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {f : Fin 1 → V} : LinearIndependent K f ↔ f 0 ≠ 0

A one-element family is linearly independent exactly when its single vector is nonzero. This is the Fin 1 companion of Mathlib's linearIndependent_fin2, which Mathlib does not have.

theorem exteriorPower.ιMulti_ne_zero {K : Type u_1} {E : Type u_2} [Field K] [AddCommGroup E] [Module K E] {k : ℕ} {v : Fin k → E} (hv : LinearIndependent K v) : (ιMulti K k) v ≠ 0

Over a field, the wedge of a linearly independent family is nonzero.

theorem exteriorPower.ιMulti_eq_zero_iff {K : Type u_1} {E : Type u_2} [Field K] [AddCommGroup E] [Module K E] {k : ℕ} (v : Fin k → E) : (ιMulti K k) v = 0 ↔ ¬LinearIndependent K v

Over a field, a wedge of k vectors vanishes exactly when they are linearly dependent.

theorem exteriorPower.ιMulti_snoc_eq_zero_iff {K : Type u_1} {E : Type u_2} [Field K] [AddCommGroup E] [Module K E] {k : ℕ} {v : Fin k → E} (hv : LinearIndependent K v) (x : E) : (ιMulti K (k + 1)) (Fin.snoc v x) = 0 ↔ x ∈ Submodule.span K (Set.range v)

The wedge criterion for membership in a span. A vector lies in the span of a linearly independent family exactly when wedging it onto that family gives 0.

theorem exteriorPower.coe_ιMulti_snoc {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k : ℕ} (v : Fin k → M) (x : M) : ↑((ιMulti R (k + 1)) (Fin.snoc v x)) = ↑((ιMulti R k) v) * (ExteriorAlgebra.ι R) x

Wedging a vector onto a wedge is multiplication in the exterior algebra.

theorem exteriorPower.ιMulti_snoc_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {k : ℕ} {c : R} {v w : Fin k → M} (h : (ιMulti R k) v = c • (ιMulti R k) w) (x : M) : (ιMulti R (k + 1)) (Fin.snoc v x) = c • (ιMulti R (k + 1)) (Fin.snoc w x)

The wedge criterion sees a wedge only up to a scalar: proportional wedges give proportional results when a further vector is wedged on.

noncomputable def exteriorPower.plucker {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (k : ℕ) (v : Fin k → ι → R) : ↑(Set.powersetCard ι k) → R

The Plücker coordinates of a family v : Fin k → (ι → R): the coordinate tuple of the wedge v 0 ∧ ⋯ ∧ v (k-1) in the basis of ⋀[R]^k (ι → R) induced by the standard basis of ι → R, indexed by the k-element subsets of ι.

Equations

• exteriorPower.plucker k v = (Module.Basis.exteriorPower k (Pi.basisFun R ι)).equivFun ((exteriorPower.ιMulti R k) v)

theorem exteriorPower.plucker_apply {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (k : ℕ) (v : Fin k → ι → R) (s : ↑(Set.powersetCard ι k)) : plucker k v s = (Matrix.of fun (i j : Fin k) => v i ((Set.powersetCard.ofFinEmbEquiv.symm s) j)).det

The Plücker coordinates are the maximal minors. The coordinate at a k-element subset s of ι is the determinant of the k × k matrix cut out of the rows v by the columns s, the columns taken in the order of ι.

theorem exteriorPower.plucker_comp_ringHom {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) : (plucker k fun (l : Fin k) => ⇑f ∘ v l) = ⇑f ∘ plucker k v

The Plücker coordinates commute with a ring homomorphism. They are determinants, so this is RingHom.map_det; it is what carries the Plücker point of a subspace along a base change.

@[simp]

theorem exteriorPower.plucker_zero {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : Fin 0 → ι → R) : plucker 0 v = 1

The empty wedge: in rank 0 there is one Plücker coordinate and it is 1.

theorem exteriorPower.plucker_one_ofSingleton {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (x : ι → R) (i : ι) : plucker 1 ![x] (Set.powersetCard.ofSingleton i) = x i

In rank 1 the Plücker coordinate at the singleton {i} is the i-th coordinate: the Plücker embedding extends the identity on points.

theorem exteriorPower.plucker_one_comp {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (x : ι → R) : plucker 1 ![x] ∘ ⇑Set.powersetCard.ofSingleton = x

In rank 1 the Plücker coordinates are the coordinates, re-indexed along Set.powersetCard.ofSingleton.

theorem exteriorPower.plucker_fin_eq_det {R : Type u_1} [CommRing R] {n : ℕ} (v : Fin n → Fin n → R) (s : ↑(Set.powersetCard (Fin n) n)) : plucker n v s = (Matrix.of v).det

In top rank there is one Plücker coordinate and it is the determinant.

theorem exteriorPower.plucker_eq_smul_iff {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (k : ℕ) (c : R) (v w : Fin k → ι → R) : plucker k v = c • plucker k w ↔ (ιMulti R k) v = c • (ιMulti R k) w

The Plücker coordinates determine the wedge: proportionality of the coordinate tuples is proportionality of the wedges.

theorem exteriorPower.plucker_smul {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (k : ℕ) (c : Fin k → R) (v : Fin k → ι → R) (s : ↑(Set.powersetCard ι k)) : plucker k (fun (i : Fin k) => c i • v i) s = (∏ i : Fin k, c i) * plucker k v s

Scaling the vectors scales the Plücker coordinates by the product of the scalars. The Plücker coordinates are a multilinear function of the family, so rescaling each vector multiplies every coordinate by the product of the scalars — the statement that a determinant is multilinear in its rows, read on the maximal minors at once.

theorem exteriorPower.plucker_eq_zero_iff {ι : Type u_2} [Fintype ι] [LinearOrder ι] {K : Type u_3} [Field K] (k : ℕ) (v : Fin k → ι → K) : plucker k v = 0 ↔ ¬LinearIndependent K v

Over a field, the Plücker coordinates of a family vanish exactly when it is linearly dependent.

theorem exteriorPower.plucker_ne_zero {ι : Type u_2} [Fintype ι] [LinearOrder ι] {K : Type u_3} [Field K] {k : ℕ} {v : Fin k → ι → K} (hv : LinearIndependent K v) : plucker k v ≠ 0

Over a field, the Plücker coordinates of a linearly independent family are not all zero.

theorem exteriorPower.plucker_one_ne_zero {ι : Type u_2} [Fintype ι] [LinearOrder ι] {K : Type u_3} [Field K] {x : ι → K} (hx : x ≠ 0) : plucker 1 ![x] ≠ 0

The Plücker coordinates of a nonzero vector, read as a one-element family, are not all zero.

theorem Submodule.linearIndependent_coe_basis {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {κ : Type u_3} {V : Submodule R M} (b : Module.Basis κ R ↥V) : LinearIndependent R fun (i : κ) => ↑(b i)

The family of vectors of M underlying a basis of a submodule is linearly independent.

theorem Submodule.span_range_coe_basis {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {κ : Type u_3} {V : Submodule R M} (b : Module.Basis κ R ↥V) : span R (Set.range fun (i : κ) => ↑(b i)) = V

The span of the vectors underlying a basis of a submodule is that submodule.

noncomputable def Submodule.pluckerPoint {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {k : ℕ} (V : Submodule K (ι → K)) (hV : Module.finrank K ↥V = k) : Projectivization K (↑(Set.powersetCard ι k) → K)

The Plücker point of a k-dimensional subspace of ι → K (Bombieri–Gubler 2.8.4; Hindry–Silverman, Exercise A.1.11(a)–(b)): the point of projective space on the k-element subsets of ι given by the Plücker coordinates of any basis of V. It does not depend on the basis; see Submodule.pluckerPoint_eq_mk.

Equations

• V.pluckerPoint hV = Projectivization.mk K (exteriorPower.plucker k fun (i : Fin k) => ↑((Module.finBasisOfFinrankEq K (↥V) hV) i)) ⋯

theorem Submodule.pluckerPoint_eq_mk {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {k : ℕ} {V : Submodule K (ι → K)} (hV : Module.finrank K ↥V = k) (b : Module.Basis (Fin k) K ↥V) (hb : (exteriorPower.plucker k fun (i : Fin k) => ↑(b i)) ≠ 0) : V.pluckerPoint hV = Projectivization.mk K (exteriorPower.plucker k fun (i : Fin k) => ↑(b i)) hb

The Plücker point is computed by every basis, not only by the chosen one.

theorem Submodule.pluckerPoint_span_range {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {k : ℕ} {v : Fin k → ι → K} (hv : LinearIndependent K v) (hV : Module.finrank K ↥(span K (Set.range v)) = k) : (span K (Set.range v)).pluckerPoint hV = Projectivization.mk K (exteriorPower.plucker k v) ⋯

The Plücker point of a span. For a linearly independent family, the Plücker point of the subspace it spans is the point defined by its Plücker coordinates.

theorem Submodule.pluckerPoint_congr {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {k : ℕ} {V W : Submodule K (ι → K)} (h : V = W) (hV : Module.finrank K ↥V = k) (hW : Module.finrank K ↥W = k) : V.pluckerPoint hV = W.pluckerPoint hW

Equal subspaces have equal Plücker points, whatever rank proofs they are given.

theorem Submodule.pluckerPoint_span_singleton {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [LinearOrder ι] {x : ι → K} (hx : x ≠ 0) (hV : Module.finrank K ↥(K ∙ x) = 1) : (K ∙ x).pluckerPoint hV = Projectivization.mk K (exteriorPower.plucker 1 ![x]) ⋯

The Plücker point of a line is the point itself, re-indexed along Set.powersetCard.ofSingleton (exteriorPower.plucker_one_comp). This is the compatibility that makes Layer 3.2's height of a subspace agree with Mathlib's height of a point on a line.

theorem Submodule.pluckerPoint_injective {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (k : ℕ) : Function.Injective fun (V : { V : Submodule K (ι → K) // Module.finrank K ↥V = k }) => (↑V).pluckerPoint ⋯

The Plücker map is an embedding (Hindry–Silverman, Exercise A.1.11(b)): distinct subspaces of the same rank have distinct Plücker points. This is what Layer 3.7 turns into Northcott for subspaces.