The degree quotients of a Clifford filtration

Mathlib's CliffordAlgebra.equivExterior identifies a Clifford algebra with its exterior-algebra model when 2 is invertible. This file proves that the equivalence respects the degree filtration, then transports the zero-form calculation of each successive quotient to an arbitrary quadratic form.

This is the degree-quotient part of the Layer 0 filtrationGradedEquiv target in the spin representations roadmap. It also identifies that equivalence with the leading-term map built in TauCeti.LinearAlgebra.CliffordAlgebra.Filtration, which reaches the same target by a different route, completing the bridge that file describes itself as having proved only half of. It does not construct the total associated-graded algebra or prove multiplication compatibility.

Main definitions

• CliffordAlgebra.equivExteriorFiltration: equivExterior restricted to one filtration step.
• CliffordAlgebra.filtrationGradedEquiv: the corresponding degree-quotient equivalence with the exterior power.

Main results

• CliffordAlgebra.equivExterior_mem_zero_form_filtration and CliffordAlgebra.equivExterior_symm_mem_filtration: equivExterior and its inverse carry each Clifford filtration step to the corresponding zero-form step and back.
• CliffordAlgebra.filtrationGradedEquiv_comp_filtrationLeadingTerm: the graded equivalence inverts Filtration.lean's leading-term map, so the two independent routes to the degree quotient are the same map, with CliffordAlgebra.filtrationLeadingTerm_eq_filtrationGradedEquiv_symm the map-level form.

References

• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 0, "The degree filtration".
• The identification of the associated graded of the Clifford filtration with the exterior algebra is the Clifford-algebra analogue of the Poincaré-Birkhoff-Witt theorem; see C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II, and H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Proposition I.1.2.
• The transport used here is Bourbaki's λ_B, Mathlib's CliffordAlgebra.changeForm: it is triangular with identity leading term rather than an antisymmetrisation, which is why the two routes agree on the nose with no scalar. See N. Bourbaki, Algèbre IX §9, and [Gri16] as cited by Mathlib's Contraction.lean.

noncomputable def CliffordAlgebra.equivExteriorFiltration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (k : ℕ) : ↥(filtration Q k) ≃ₗ[R] ↥(filtration 0 k)

equivExterior restricted to a Clifford filtration step.

Equations

• CliffordAlgebra.equivExteriorFiltration Q k = (CliffordAlgebra.equivExterior Q).ofSubmodules (CliffordAlgebra.filtration Q k) (CliffordAlgebra.filtration 0 k) ⋯

@[simp]

theorem CliffordAlgebra.coe_equivExteriorFiltration_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (k : ℕ) (x : ↥(filtration Q k)) : ↑((equivExteriorFiltration Q k) x) = (equivExterior Q) ↑x

Coercing the restricted exterior equivalence is the ambient equivExterior map.

@[simp]

theorem CliffordAlgebra.coe_equivExteriorFiltration_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (k : ℕ) (x : ↥(filtration 0 k)) : ↑((equivExteriorFiltration Q k).symm x) = (equivExterior Q).symm ↑x

Coercing the inverse restricted exterior equivalence is the ambient inverse map.

theorem CliffordAlgebra.equivExterior_mem_zero_form_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {k : ℕ} {x : CliffordAlgebra Q} (hx : x ∈ filtration Q k) : (equivExterior Q) x ∈ filtration 0 k

equivExterior carries each Clifford filtration step into the corresponding zero-form step.

theorem CliffordAlgebra.equivExterior_symm_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {k : ℕ} {x : ExteriorAlgebra R M} (hx : x ∈ filtration 0 k) : (equivExterior Q).symm x ∈ filtration Q k

The inverse of equivExterior carries each zero-form filtration step back into the corresponding Clifford step.

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

The successive degree quotient of a Clifford algebra is the corresponding exterior power.

Equations

• CliffordAlgebra.filtrationGradedEquiv Q k = (CliffordAlgebra.equivExteriorFiltrationQuotient✝ Q k).trans (CliffordAlgebra.zeroFormFiltrationQuotientEquivExteriorPower k)

@[simp]

theorem CliffordAlgebra.filtrationGradedEquiv_apply_mk {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (k : ℕ) (x : ↥(filtration Q (k + 1))) : (filtrationGradedEquiv Q k) (Submodule.Quotient.mk x) = (zeroFormFiltrationQuotientEquivExteriorPower k) (Submodule.Quotient.mk ⟨(equivExterior Q) ↑x, ⋯⟩)

On quotient representatives, filtrationGradedEquiv first applies equivExterior.

@[simp]

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

The inverse graded equivalence sends an exterior element to the quotient class of its preimage under equivExterior.

theorem CliffordAlgebra.filtrationGradedEquiv_comp_filtrationLeadingTerm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (k : ℕ) : ↑(filtrationGradedEquiv Q k) ∘ₗ filtrationLeadingTerm Q k = LinearMap.id

The graded equivalence undoes the leading-term map. Together with filtrationLeadingTerm_surjective, which holds over any CommRing, this identifies the two independent routes Filtration.lean and this file take to the degree-k + 1 quotient.

@[simp]

theorem CliffordAlgebra.filtrationGradedEquiv_filtrationLeadingTerm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (k : ℕ) (x : ↥(⋀[R]^(k + 1) M)) : (filtrationGradedEquiv Q k) ((filtrationLeadingTerm Q k) x) = x

The pointwise form, which is the one simp can use.

theorem CliffordAlgebra.filtrationLeadingTerm_eq_filtrationGradedEquiv_symm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (k : ℕ) : filtrationLeadingTerm Q k = ↑(filtrationGradedEquiv Q k).symm

The leading-term map is filtrationGradedEquiv's inverse.