The Plücker point of a subspace

Let K be a field and ι a finite linearly ordered type. A subspace U of K^ι of dimension p determines a point of the projective space over K^(powersetCard ι p): the class of the Plücker coordinates (the maximal minors) of any basis of U. A change of basis multiplies the coordinates by its determinant, so the point does not depend on the basis. Conversely the point determines the subspace: a vector v lies in the span of a linearly independent family x exactly when the exterior product v ∧ x 0 ∧ ⋯ ∧ x (p - 1) vanishes, and that product is linear in the exterior product of x. This is the Plücker embedding of the Grassmannian of p-dimensional subspaces into projective space.

Heights of subspaces are heights of these points.

Main definitions

• Submodule.relativePluckerPoint U: the Plücker point of a subspace U of ι → K, in the projective space over powersetCard ι (finrank K U) → K.

Main results

• TauCeti.mk_plucker_eq_mk_plucker_iff: two linearly independent families of p vectors have proportional Plücker coordinates exactly when they span the same subspace.
• Submodule.relativePluckerPoint_eq_mk: the Plücker point of U is the class of the Plücker coordinates of any basis of U.
• Submodule.finrank_relativePluckerPoint_injective: a subspace is determined by its dimension and its Plücker point.

References

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

theorem TauCeti.mk_plucker_eq_mk_plucker_iff {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] {p : ℕ} {x y : Fin p → ι → K} (hx : LinearIndependent K x) (hy : LinearIndependent K y) : Projectivization.mk K (plucker x) ⋯ = Projectivization.mk K (plucker y) ⋯ ↔ Submodule.span K (Set.range x) = Submodule.span K (Set.range y)

Two linearly independent families of p vectors in ι → K have proportional Plücker coordinates exactly when they span the same subspace.

noncomputable def Submodule.relativePluckerPoint {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] (U : Submodule K (ι → K)) : Projectivization K (↑(Set.powersetCard ι (Module.finrank K ↥U)) → K)

The Plücker point of a subspace U of ι → K: the point of the projective space over powersetCard ι (finrank K U) → K given by the Plücker coordinates of a basis of U. It does not depend on the basis, by relativePluckerPoint_eq_mk.

theorem Submodule.relativePluckerPoint_eq_mk {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] {U : Submodule K (ι → K)} (b : Module.Basis (Fin (Module.finrank K ↥U)) K ↥U) : U.relativePluckerPoint = Projectivization.mk K (TauCeti.plucker fun (i : Fin (Module.finrank K ↥U)) => ↑(b i)) ⋯

The Plücker point of U is the class of the Plücker coordinates of any basis of U.

theorem Submodule.finrank_relativePluckerPoint_injective {ι : Type u_1} {K : Type u_2} [LinearOrder ι] [Finite ι] [Field K] : Function.Injective fun (U : Submodule K (ι → K)) => ⟨Module.finrank K ↥U, U.relativePluckerPoint⟩

A subspace is determined by its dimension together with its Plücker point: the Plücker point is injective on the subspaces of each fixed dimension.