Exterior creation and contraction generate all endomorphisms

For a finite free module, left exterior multiplication and contraction by dual vectors generate the full endomorphism algebra of its exterior algebra.

Main result

• TauCeti.ExteriorAlgebra.creation_contraction_adjoin_eq_top: creation and contraction generate every endomorphism.

References

• Spin representations roadmap

theorem TauCeti.ExteriorAlgebra.creation_contraction_adjoin_eq_top {K : Type u} [CommRing K] {W : Type v} [AddCommGroup W] [Module K W] [Module.Free K W] [Module.Finite K W] : Algebra.adjoin K ((Set.range fun (x : W) => LinearMap.mulLeft K ((ExteriorAlgebra.ι K) x)) ∪ Set.range fun (d : Module.Dual K W) => CliffordAlgebra.contractLeft d) = ⊤

Exterior creation and contraction generate every endomorphism of a finite free module's exterior algebra.