theorem GrassmannianProjective.orderEmb_fin_eq_id (n : ℕ) (f : Fin n ↪o Fin n) (i : Fin n) : f i = i

Any order embedding Fin n ↪o Fin n is the identity, since a strictly increasing bijection on Fin n must be the identity.

theorem GrassmannianProjective.ιMulti_basis_ne_zero {K : Type u_1} [Field K] {n : ℕ} {W : Type u_2} [AddCommGroup W] [Module K W] (b : Module.Basis (Fin n) K W) : ((exteriorPower.ιMulti K n) fun (i : Fin n) => b i) ≠ 0

The exterior power of a basis is nonzero: e_1 ∧ ... ∧ e_n ≠ 0.

def GrassmannianProjective.SubspaceGr (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] (k : ℕ) : Type u_3

The Grassmannian Gr(k, V) as a set of k-dimensional subspaces of V.

noncomputable def GrassmannianProjective.subspaceBasis (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Finite K V] (k : ℕ) (W : Submodule K V) (hk : Module.finrank K ↥W = k) : Module.Basis (Fin k) K ↥W

Choose a basis Fin k → W for a k-dimensional subspace W of V.

noncomputable def GrassmannianProjective.pluckerCoord (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Finite K V] (k : ℕ) (W : Submodule K V) (hk : Module.finrank K ↥W = k) : ↥(⋀[K]^k V)

Plücker coordinate of W: the image of e_1 ∧ ... ∧ e_k in ⋀^k V under the inclusion.

theorem GrassmannianProjective.plucker_coord_ne_zero (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Finite K V] (k : ℕ) (W : Submodule K V) (hk : Module.finrank K ↥W = k) : pluckerCoord K V k W hk ≠ 0

The Plücker coordinate of a k-dimensional subspace is nonzero, so it defines a point in P(⋀^k V).

noncomputable def GrassmannianProjective.pluckerMap (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Finite K V] (k : ℕ) : SubspaceGr K V k → Projectivization K ↥(⋀[K]^k V)

Plücker map Gr(k, V) → P(⋀^k V) sending W to the projective class of e_1 ∧ ... ∧ e_k.

def GrassmannianProjective.IsDecomposableExtPower (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] (k : ℕ) (ω : ↥(⋀[K]^k V)) : Prop

A k-vector ω ∈ ⋀^k V is decomposable if it can be written as a wedge v_1 ∧ ... ∧ v_k.

def GrassmannianProjective.DecomposableProjective (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] (k : ℕ) : Set (Projectivization K ↥(⋀[K]^k V))

The locus of decomposable classes in P(⋀^k V), i.e. the image of the Plücker map.

theorem GrassmannianProjective.plucker_embedding_injective (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (k : ℕ) : Function.Injective (pluckerMap K V k)

The Plücker map is injective: distinct subspaces give distinct projective classes.

theorem GrassmannianProjective.plucker_image_eq_decomposable (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (k : ℕ) : Set.range (pluckerMap K V k) = DecomposableProjective K V k

Image of the Plücker map equals the decomposable locus.

theorem GrassmannianProjective.grassmannian_is_projective_variety (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (k : ℕ) : Function.Injective (pluckerMap K V k) ∧ Set.range (pluckerMap K V k) = DecomposableProjective K V k ∧ Module.finrank K ↥(⋀[K]^k V) = (Module.finrank K V).choose k

Thm 4.1 (Lec 4): The Grassmannian Gr(k, n) embeds as a closed subvariety of P^{C(n,k)-1} via Plücker, exhibited here by injectivity, image, and ambient dimension.

theorem GrassmannianProjective.plucker_ambient_dim (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (k : ℕ) : Module.finrank K ↥(⋀[K]^k V) = (Module.finrank K V).choose k

Ambient projective dimension: dim ⋀^k V = C(n, k) where n = dim V.

theorem GrassmannianProjective.plucker_target_finrank (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (k n : ℕ) (hdim : Module.finrank K V = n) : Module.finrank K ↥(⋀[K]^k V) = n.choose k

Specialization of plucker_ambient_dim to a given ambient dimension n.

def GrassmannianProjective.IsZariskiClosedByQuadratics (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] (k : ℕ) (S : Set (Projectivization K ↥(⋀[K]^k V))) : Prop

A subset of P(⋀^k V) is Zariski closed by quadratics if it is the zero locus of homogeneous degree-2 polynomial functions (the Plücker relations).

theorem GrassmannianProjective.plucker_is_closed_embedding (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (k : ℕ) : IsZariskiClosedByQuadratics K V k (DecomposableProjective K V k)

The image of the Plücker embedding is cut out by quadratic Plücker relations.

def GrassmannianProjective.IsDecomposableDeg2 {K : Type u_2} [CommRing K] {M : Type u_3} [AddCommGroup M] [Module K M] (ω : ExteriorAlgebra K M) : Prop

A degree-2 element of the exterior algebra is decomposable if it equals a single wedge v₁ ∧ v₂.

theorem GrassmannianProjective.ι_anticomm_ext {K : Type u_2} [CommRing K] {M : Type u_3} [AddCommGroup M] [Module K M] (x y : M) : (ExteriorAlgebra.ι K) x * (ExteriorAlgebra.ι K) y = -((ExteriorAlgebra.ι K) y * (ExteriorAlgebra.ι K) x)

Anti-commutativity of the embedding ι : M → ΛM: ι x ∧ ι y = -(ι y ∧ ι x).

theorem GrassmannianProjective.wedge_sq_zero_decomp {K : Type u_2} [CommRing K] {M : Type u_3} [AddCommGroup M] [Module K M] (v₁ v₂ : M) : (ExteriorAlgebra.ι K) v₁ * (ExteriorAlgebra.ι K) v₂ * ((ExteriorAlgebra.ι K) v₁ * (ExteriorAlgebra.ι K) v₂) = 0

A pure wedge squares to zero: (v₁ ∧ v₂)^2 = 0 in the exterior algebra.

theorem GrassmannianProjective.wedge_sq_zero_of_isDecomposableDeg2 {K : Type u_2} [CommRing K] {M : Type u_3} [AddCommGroup M] [Module K M] {ω : ExteriorAlgebra K M} (h : IsDecomposableDeg2 ω) : ω * ω = 0

Decomposable degree-2 elements square to zero (necessary condition for the Plücker relation).

theorem GrassmannianProjective.ι_pair_comm_deg2 {K : Type u_2} [CommRing K] {M : Type u_3} [AddCommGroup M] [Module K M] (a b c d : M) : (ExteriorAlgebra.ι K) a * (ExteriorAlgebra.ι K) b * ((ExteriorAlgebra.ι K) c * (ExteriorAlgebra.ι K) d) = (ExteriorAlgebra.ι K) c * (ExteriorAlgebra.ι K) d * ((ExteriorAlgebra.ι K) a * (ExteriorAlgebra.ι K) b)

Two degree-2 wedges commute in the exterior algebra (graded commutativity, even × even).

theorem GrassmannianProjective.wedge_sq_sum_decomp_pair {K : Type u_2} [CommRing K] {M : Type u_3} [AddCommGroup M] [Module K M] (v₁ v₂ v₃ v₄ : M) : ((ExteriorAlgebra.ι K) v₁ * (ExteriorAlgebra.ι K) v₂ + (ExteriorAlgebra.ι K) v₃ * (ExteriorAlgebra.ι K) v₄) * ((ExteriorAlgebra.ι K) v₁ * (ExteriorAlgebra.ι K) v₂ + (ExteriorAlgebra.ι K) v₃ * (ExteriorAlgebra.ι K) v₄) = 2 * ((ExteriorAlgebra.ι K) v₁ * (ExteriorAlgebra.ι K) v₂ * ((ExteriorAlgebra.ι K) v₃ * (ExteriorAlgebra.ι K) v₄))

For ω = v₁ ∧ v₂ + v₃ ∧ v₄, the square ω ∧ ω equals 2 (v₁ ∧ v₂ ∧ v₃ ∧ v₄).

theorem GrassmannianProjective.skew_form_normal_form_dim4 {K : Type u_2} [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (hdim : Module.finrank K V = 4) (ω : ExteriorAlgebra K V) (hω2 : ω ∈ ⋀[K]^2 V) : (∃ (v₁ : V) (v₂ : V), ω = (ExteriorAlgebra.ι K) v₁ * (ExteriorAlgebra.ι K) v₂) ∨ ∃ (v₁ : V) (v₂ : V) (v₃ : V) (v₄ : V), LinearIndependent K ![v₁, v₂, v₃, v₄] ∧ ω = (ExteriorAlgebra.ι K) v₁ * (ExteriorAlgebra.ι K) v₂ + (ExteriorAlgebra.ι K) v₃ * (ExteriorAlgebra.ι K) v₄

Normal form of skew forms in dim 4: a 2-form is either a pure wedge v₁ ∧ v₂ or a sum of two wedges v₁ ∧ v₂ + v₃ ∧ v₄ on a linearly independent basis.

theorem GrassmannianProjective.product_eq_ιMulti {K : Type u_2} [Field K] {V : Type u_3} [AddCommGroup V] [Module K V] (v₁ v₂ v₃ v₄ : V) : (ExteriorAlgebra.ι K) v₁ * (ExteriorAlgebra.ι K) v₂ * ((ExteriorAlgebra.ι K) v₃ * (ExteriorAlgebra.ι K) v₄) = (ExteriorAlgebra.ιMulti K 4) ![v₁, v₂, v₃, v₄]

Iterated product of four ι's coincides with ιMulti K 4 applied to a 4-tuple.

theorem GrassmannianProjective.ιMulti_ne_zero_of_linearIndependent {K : Type u_2} [Field K] {V : Type u_3} [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (hdim : Module.finrank K V = 4) (v : Fin 4 → V) (hli : LinearIndependent K v) : (ExteriorAlgebra.ιMulti K 4) v ≠ 0

A linearly independent 4-tuple in a 4-dimensional space wedges to a nonzero top form.

theorem GrassmannianProjective.alternating_form_classification_dim4_gr {K : Type u_2} [Field K] [CharZero K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (hdim : Module.finrank K V = 4) (ω : ExteriorAlgebra K V) (hω2 : ω ∈ ⋀[K]^2 V) (hωω : ω * ω = 0) : IsDecomposableDeg2 ω

Lemma 6 converse for dim V = 4 (char zero): if ω ∈ ⋀^2 V satisfies the Plücker relation ω ∧ ω = 0, then ω is decomposable.

theorem GrassmannianProjective.gr24_plucker_target_dim (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (hdim : Module.finrank K V = 4) : Module.finrank K ↥(⋀[K]^2 V) = 6

The Plücker target for Gr(2, 4) has dimension C(4, 2) = 6.

theorem GrassmannianProjective.extPower_four_dim_one (K : Type u_2) [Field K] (V : Type u_3) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (hdim : Module.finrank K V = 4) : Module.finrank K ↥(⋀[K]^4 V) = 1

⋀^4 V is one-dimensional when dim V = 4.

theorem GrassmannianProjective.ιMulti_stdBasis_nonzero {K : Type u_2} [Field K] : (ExteriorAlgebra.ιMulti K 4) ⇑(Pi.basisFun K (Fin 4)) ≠ 0

The wedge of standard basis vectors e_0 ∧ e_1 ∧ e_2 ∧ e_3 in (K^4) is nonzero.

theorem GrassmannianProjective.basis_product_is_ιMulti {K : Type u_2} [Field K] : (ExteriorAlgebra.ι K) (Pi.single 0 1) * (ExteriorAlgebra.ι K) (Pi.single 1 1) * ((ExteriorAlgebra.ι K) (Pi.single 2 1) * (ExteriorAlgebra.ι K) (Pi.single 3 1)) = (ExteriorAlgebra.ιMulti K 4) ⇑(Pi.basisFun K (Fin 4))

The product of ι on the four standard basis vectors equals the top wedge e_0 ∧ e_1 ∧ e_2 ∧ e_3.

theorem GrassmannianProjective.non_decomp_wedge_sq_ne_zero {K : Type u_2} [Field K] [CharZero K] : ((ExteriorAlgebra.ι K) (Pi.single 0 1) * (ExteriorAlgebra.ι K) (Pi.single 1 1) + (ExteriorAlgebra.ι K) (Pi.single 2 1) * (ExteriorAlgebra.ι K) (Pi.single 3 1)) * ((ExteriorAlgebra.ι K) (Pi.single 0 1) * (ExteriorAlgebra.ι K) (Pi.single 1 1) + (ExteriorAlgebra.ι K) (Pi.single 2 1) * (ExteriorAlgebra.ι K) (Pi.single 3 1)) ≠ 0

The sum e_0 ∧ e_1 + e_2 ∧ e_3 in ⋀^2 (K^4) has nonzero square, hence it is not decomposable.

theorem GrassmannianProjective.gr24_is_quadric_in_P5 (K : Type u_4) [Field K] [CharZero K] (V : Type u_5) [AddCommGroup V] [Module K V] [Module.Free K V] [Module.Finite K V] (hdim : Module.finrank K V = 4) : Module.finrank K ↥(⋀[K]^2 V) = 6 ∧ Function.Injective (pluckerMap K V 2) ∧ ∀ ω ∈ ⋀[K]^2 V, ω * ω = 0 → IsDecomposableDeg2 ω

Plücker embedding for Gr(2, 4): ambient P^5, injective Plücker map, and Gr(2, 4) is the quadric {ω : ω ∧ ω = 0} in P(⋀^2 V) (char zero, dim V = 4).