theorem PluckerGr24.ι_anticomm {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (x y : M) : (ExteriorAlgebra.ι R) x * (ExteriorAlgebra.ι R) y = -((ExteriorAlgebra.ι R) y * (ExteriorAlgebra.ι R) x)

Anticommutativity in the exterior algebra: for x, y in M, ι(x) ι(y) = -ι(y) ι(x).

theorem PluckerGr24.wedge_sq_zero_of_decomposable {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (v₁ v₂ : M) : (ExteriorAlgebra.ι R) v₁ * (ExteriorAlgebra.ι R) v₂ * ((ExteriorAlgebra.ι R) v₁ * (ExteriorAlgebra.ι R) v₂) = 0

A decomposable 2-vector v_1 ∧ v_2 satisfies (v_1 ∧ v_2)^2 = 0 in the exterior algebra (Plücker forward direction).

def PluckerGr24.IsDecomposable2 {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (ω : ExteriorAlgebra R M) : Prop

A 2-vector ω is decomposable if it can be written as v_1 ∧ v_2 for some vectors.

theorem PluckerGr24.wedge_sq_zero_of_isDecomposable2 {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ω : ExteriorAlgebra R M} (h : IsDecomposable2 ω) : ω * ω = 0

Every decomposable 2-vector squares to zero in the exterior algebra.

theorem PluckerGr24.ι_pair_comm {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (a b c d : M) : (ExteriorAlgebra.ι R) a * (ExteriorAlgebra.ι R) b * ((ExteriorAlgebra.ι R) c * (ExteriorAlgebra.ι R) d) = (ExteriorAlgebra.ι R) c * (ExteriorAlgebra.ι R) d * ((ExteriorAlgebra.ι R) a * (ExteriorAlgebra.ι R) b)

Graded commutativity for products of two pairs: (a∧b)(c∧d) = (c∧d)(a∧b) since even-degree elements commute in the exterior algebra.

theorem PluckerGr24.wedge_sq_sum_decomposable {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (v₁ v₂ v₃ v₄ : M) : ((ExteriorAlgebra.ι R) v₁ * (ExteriorAlgebra.ι R) v₂ + (ExteriorAlgebra.ι R) v₃ * (ExteriorAlgebra.ι R) v₄) * ((ExteriorAlgebra.ι R) v₁ * (ExteriorAlgebra.ι R) v₂ + (ExteriorAlgebra.ι R) v₃ * (ExteriorAlgebra.ι R) v₄) = 2 * ((ExteriorAlgebra.ι R) v₁ * (ExteriorAlgebra.ι R) v₂ * ((ExteriorAlgebra.ι R) v₃ * (ExteriorAlgebra.ι R) v₄))

For a sum of two decomposable 2-vectors, the square equals 2 (v_1∧v_2) (v_3∧v_4).

theorem PluckerGr24.exteriorPower_two_finrank_of_four (k : Type u_1) [Field k] (V : Type u_2) [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

For a 4-dimensional vector space V, ⋀²V has dimension 6 = C(4,2), giving the ambient P^5 for the Plücker embedding of Gr(2,4).

theorem PluckerGr24.exteriorPower_finrank (k : Type u_1) [Field k] (V : Type u_2) [AddCommGroup V] [Module k V] [Module.Free k V] [Module.Finite k V] {n : ℕ} : Module.finrank k ↥(⋀[k]^n V) = (Module.finrank k V).choose n

General dimension formula: dim ⋀^n V = C(dim V, n).

theorem PluckerGr24.exteriorPower_four_finrank_of_four (k : Type u_1) [Field k] (V : Type u_2) [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

For a 4-dimensional vector space V, ⋀⁴V is 1-dimensional.

theorem PluckerGr24.decomposable_iff_wedge_sq_zero_forward {k : Type u_1} [Field k] (ω : ExteriorAlgebra k (Fin 4 → k)) (hω : IsDecomposable2 ω) : ω * ω = 0

Forward Plücker relation in k^4: decomposable 2-vectors square to zero.

theorem PluckerGr24.ιMulti_stdBasis_ne_zero {k : Type u_1} [Field k] : (ExteriorAlgebra.ιMulti k 4) ⇑(Pi.basisFun k (Fin 4)) ≠ 0

The wedge of the four standard basis vectors of k^4 is nonzero (it gives a basis of the 1-dimensional space ⋀⁴(k^4)).

theorem PluckerGr24.product_basis_eq_ιMulti {k : Type u_1} [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 e_0 ∧ e_1 ∧ e_2 ∧ e_3 of the four standard basis vectors equals the top wedge ιMulti(e_0, e_1, e_2, e_3).

theorem PluckerGr24.non_decomposable_wedge_sq_ne_zero {k : Type u_1} [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 2-vector e_0∧e_1 + e_2∧e_3 in k^4 squares to a nonzero multiple of the volume form, witnessing a non-decomposable element ruled out by the Plücker relation.

theorem PluckerGr24.isDecomposable2_of_wedge_sq_zero_dim_four {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [Module.Free k V] [Module.Finite k V] [CharZero k] (hdim : Module.finrank k V = 4) {ω : ExteriorAlgebra k V} (hω2 : ω ∈ ⋀[k]^2 V) (hsq : ω * ω = 0) : IsDecomposable2 ω

Converse Plücker relation in dimension 4 (char 0): a 2-vector ω ∈ ⋀²V with ω∧ω = 0 is decomposable.

theorem PluckerGr24.converse_wedge_sq_zero {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [Module.Free k V] [Module.Finite k V] [CharZero k] (hdim : Module.finrank k V = 4) {ω : ExteriorAlgebra k V} (hω2 : ω ∈ ⋀[k]^2 V) (hsq : ω * ω = 0) : IsDecomposable2 ω

Converse to the Plücker relation in dim 4: ω∧ω = 0 implies ω is decomposable.

theorem PluckerGr24.decomposable_iff_wedge_sq_zero {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] [Module.Free k V] [Module.Finite k V] [CharZero k] (hdim : Module.finrank k V = 4) {ω : ExteriorAlgebra k V} (hω2 : ω ∈ ⋀[k]^2 V) : IsDecomposable2 ω ↔ ω * ω = 0

Plücker characterization in dim 4: a 2-vector is decomposable iff its wedge square vanishes — the defining equations of Gr(2,4) ⊂ P^5.

theorem PluckerGr24.gr24_lives_in_P5 (k : Type u_1) [Field k] [CharZero k] (V : Type u_2) [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 (GrassmannianProjective.pluckerMap k V 2) ∧ Set.range (GrassmannianProjective.pluckerMap k V 2) = GrassmannianProjective.DecomposableProjective k V 2 ∧ ∀ ω ∈ ⋀[k]^2 V, ω * ω = 0 → IsDecomposable2 ω

The Plücker embedding Gr(2,4) ↪ P^5 (Theorem 4.1, Lemma 6): for a 4-dimensional V, ⋀²V is 6-dimensional, the Plücker map is injective, and its image equals the set of decomposable 2-vectors, which is cut out by the Plücker quadratic relation ω∧ω = 0.