The zero-form Clifford filtration

When the quadratic form is zero, its Clifford algebra is the exterior algebra. This file identifies the Clifford degree filtration with the sum of exterior degrees up to the same bound, then uses the exterior algebra's internal grading to identify each successive filtration quotient with the corresponding exterior power.

This is the zero-form side of the Layer 0 filtrationGradedEquiv target in the spin representations roadmap. The generic change-of-form transport belongs in TauCeti.LinearAlgebra.CliffordAlgebra.Filtration.

Main results

• CliffordAlgebra.exteriorPower_succ_disjoint_zero_form_filtration: degree k + 1 is disjoint from the lower zero-form filtration.
• CliffordAlgebra.zeroFormFiltrationQuotientEquivExteriorPower: the successive zero-form filtration quotient is the degree k + 1 exterior power.

References

• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 0, "The degree filtration".

theorem CliffordAlgebra.exteriorPower_succ_disjoint_zero_form_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (k : ℕ) : Disjoint (⋀[R]^(k + 1) M) (filtration 0 k)

The degree k + 1 exterior power is disjoint from the lower zero-form filtration.

noncomputable def CliffordAlgebra.zeroFormFiltrationQuotientEquivExteriorPower {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (k : ℕ) : TauCeti.Algebra.wordFiltration.GradedPiece (ι 0) (k + 1) ≃ₗ[R] ↥(⋀[R]^(k + 1) M)

The successive zero-form Clifford filtration quotient is the degree k + 1 exterior power.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CliffordAlgebra.zeroFormFiltrationQuotientEquivExteriorPower_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (k : ℕ) (x : ↥(⋀[R]^(k + 1) M)) : (zeroFormFiltrationQuotientEquivExteriorPower k).symm x = Submodule.Quotient.mk ⟨↑x, ⋯⟩

The inverse quotient equivalence sends a degree k + 1 exterior element to its canonical quotient class.

@[simp]

theorem CliffordAlgebra.zeroFormFiltrationQuotientEquivExteriorPower_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (k : ℕ) (x : ↥(⋀[R]^(k + 1) M)) : (zeroFormFiltrationQuotientEquivExteriorPower k) (Submodule.Quotient.mk ⟨↑x, ⋯⟩) = x

The quotient equivalence sends the canonical class of a degree k + 1 exterior element to that element.