The degree filtration of a Clifford algebra

A Clifford algebra carries two different degree structures, one grading and one filtration, and it is worth keeping them apart. Mathlib already has the ℤ/2-grading CliffordAlgebra.evenOdd, which is a genuine GradedAlgebra: the Clifford relation ι Q m * ι Q m = Q m preserves the parity of the number of generators, so parity descends to the quotient. It does not preserve the number of generators, so there is no ℕ-grading; what survives is an increasing filtration by the number of generators needed to write an element.

This file builds that filtration. CliffordAlgebra.filtration Q k is the R-submodule spanned by the products ι Q v₁ * ⋯ * ι Q vₙ with n ≤ k, the empty product 1 included, so that filtration Q 0 is the module of scalars and filtration Q 1 adjoins the generators. It is increasing, multiplicative (filtration Q i * filtration Q j = filtration Q (i + j)), exhausts the algebra, and is preserved by the grade involution, by reversal, and by the functoriality of the Clifford algebra in the quadratic form.

The construction itself is not special to Clifford algebras: filtration is TauCeti.Algebra.wordFiltration specialized to ι Q, and the lemmas below that do not use the Clifford relation are specializations of the generic ones. Its successive quotients use TauCeti.Algebra.wordFiltration.GradedPiece; the universal enveloping algebra carries the same construction as its PBW filtration.

Following the roadmap, the filtration is not the submodule power LinearMap.range (ι Q) ^ k: powers of a submodule of a noncommutative algebra collect the products of exactly k generators. The relation between the two is CliffordAlgebra.filtration_eq_iSup_pow, which writes filtration Q k as the supremum of those powers over i ≤ k; this is the sense in which the filtration is the "at most k" companion of Mathlib's evenOdd, whose definition is the analogous supremum over the i of a fixed parity.

Main definitions

• CliffordAlgebra.filtration Q k: the span of the products of at most k generators.

Main results

• CliffordAlgebra.prod_map_ι_mem_filtration and CliffordAlgebra.filtration_le_iff: the products of at most k generators lie in the k-th step and generate it, which is how memberships and bounds are proved.
• CliffordAlgebra.filtration_eq_pow: the defining equation, as the k-th power of the scalars together with LinearMap.range (ι Q).
• CliffordAlgebra.filtration_mul: the filtration is multiplicative, and in fact exactly so: filtration Q i * filtration Q j = filtration Q (i + j). This is the statement that makes the associated graded object an algebra, and it is the prerequisite the roadmap asks for before anything downstream; CliffordAlgebra.filtration_pow is its iterate and CliffordAlgebra.mul_mem_filtration its elementwise form.
• CliffordAlgebra.filtration_succ_eq_sup: the recursion for the successor step.
• CliffordAlgebra.filtration_eq_top_of_finrank_le: over a field, the filtration of a finite-dimensional space is exhausted at its dimension.
• CliffordAlgebra.filtration_eq_iSup_pow: the comparison with the submodule powers of LinearMap.range (ι Q).
• CliffordAlgebra.filtrationLeadingTerm and CliffordAlgebra.filtrationLeadingTerm_surjective: the exterior-power leading-term map onto each successive filtration quotient. It is surjective over any CommRing; when 2 is invertible CliffordAlgebra.filtrationGradedEquiv_comp_filtrationLeadingTerm identifies it with the inverse of the graded equivalence.
• CliffordAlgebra.iSup_filtration_eq_top: the filtration is exhaustive.
• CliffordAlgebra.involute_mem_filtration, CliffordAlgebra.reverse_mem_filtration and CliffordAlgebra.map_mem_filtration: the filtration is preserved by the grade involution, by reversal, and by an isometry of quadratic forms.
• CliffordAlgebra.contractLeft_mem_filtration_succ and CliffordAlgebra.contractLeft_mem_filtration, CliffordAlgebra.changeForm_mem_filtration, and CliffordAlgebra.changeFormEquiv_map_filtration and CliffordAlgebra.changeForm_mem_filtration_iff: contraction and change of quadratic form respect the filtration, contraction lowers every positive step by one, and the change-form equivalence transports every step exactly.
• CliffordAlgebra.changeForm_prod_map_ι_sub_prod_map_ι_mem_filtration: change of form has identity symbol, that is, it moves a word of generators only by terms two filtration degrees lower.
• CliffordAlgebra.fg_filtration: each step is a finitely generated module when M is.

References

• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 0, "The degree filtration".
• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I.

@[reducible, inline]

abbrev CliffordAlgebra.filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (k : ℕ) : Submodule R (CliffordAlgebra Q)

The degree filtration of a Clifford algebra: filtration Q k is the R-submodule spanned by the products ι Q v₁ * ⋯ * ι Q vₙ of at most k generators, the empty product 1 included.

This is deliberately not the submodule power LinearMap.range (ι Q) ^ k, which spans the products of exactly k generators; see filtration_eq_iSup_pow for the comparison.

This is TauCeti.Algebra.wordFiltration specialized to ι Q. It is an abbrev, so that the generic construction of TauCeti/Algebra/WordFiltration/AssociatedGraded.lean applies to the Clifford filtration: instance synthesis and the rewriting tactics only see through reducible definitions.

Equations

• CliffordAlgebra.filtration Q k = TauCeti.Algebra.wordFiltration (CliffordAlgebra.ι Q) k

theorem CliffordAlgebra.filtration_eq_pow {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (k : ℕ) : filtration Q k = (1 ⊔ (ι Q).range) ^ k

The defining equation of the filtration: degree k is the k-th submodule power of the scalars together with LinearMap.range (ι Q). Contrast filtration_eq_iSup_pow, the comparison with the powers of LinearMap.range (ι Q) alone.

theorem CliffordAlgebra.prod_map_ι_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {k : ℕ} {l : List M} (hl : l.length ≤ k) : (List.map (⇑(ι Q)) l).prod ∈ filtration Q k

A product of at most k generators lies in the k-th step of the filtration. This is the generating family, so most filtration memberships reduce to it.

theorem CliffordAlgebra.filtration_le_iff {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {k : ℕ} {p : Submodule R (CliffordAlgebra Q)} : filtration Q k ≤ p ↔ ∀ (l : List M), l.length ≤ k → (List.map (⇑(ι Q)) l).prod ∈ p

The k-th step of the filtration is spanned by the products of at most k generators, so a submodule contains it exactly when it contains those products. This is Submodule.span_le in the form in which it applies to filtration.

theorem CliffordAlgebra.filtration_mono {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : Monotone (filtration Q)

The filtration is increasing: a product of at most i generators is a product of at most j of them whenever i ≤ j.

theorem CliffordAlgebra.algebraMap_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (r : R) (k : ℕ) : (algebraMap R (CliffordAlgebra Q)) r ∈ filtration Q k

Scalars lie in every step of the filtration, being multiples of the empty product.

theorem CliffordAlgebra.ι_mem_filtration_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) : (ι Q) m ∈ filtration Q 1

A generator is a product of one generator, so it lies in the first step.

theorem CliffordAlgebra.ι_range_le_filtration_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : (ι Q).range ≤ filtration Q 1

The submodule form of ι_mem_filtration_one: all of LinearMap.range (ι Q) lies in the first step.

theorem CliffordAlgebra.ι_mul_ι_mem_filtration_two {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a b : M) : (ι Q) a * (ι Q) b ∈ filtration Q 2

A product of two generators lies in the second step. This is the membership the roadmap's bivectors use.

theorem CliffordAlgebra.filtration_mul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (i j : ℕ) : filtration Q i * filtration Q j = filtration Q (i + j)

The filtration is multiplicative, and exactly so. Concatenating a product of at most i generators with a product of at most j generators gives a product of at most i + j of them, and conversely a product of at most i + j generators splits after its i-th factor. In particular the associated graded object of the filtration is an algebra.

theorem CliffordAlgebra.mul_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {i j : ℕ} {x y : CliffordAlgebra Q} (hx : x ∈ filtration Q i) (hy : y ∈ filtration Q j) : x * y ∈ filtration Q (i + j)

The elementwise form of filtration_mul: a product of an element of the i-th step and an element of the j-th step lies in the i + j-th step.

theorem CliffordAlgebra.filtration_pow {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (i n : ℕ) : filtration Q i ^ n = filtration Q (i * n)

Iterating filtration_mul: the n-th submodule power of the i-th step is the i * n-th step.

theorem CliffordAlgebra.prod_map_ι_mem_pow {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (l : List M) : (List.map (⇑(ι Q)) l).prod ∈ (ι Q).range ^ l.length

A product of exactly n generators lies in the n-th submodule power of LinearMap.range (ι Q).

theorem CliffordAlgebra.ι_range_pow_le_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (n : ℕ) : (ι Q).range ^ n ≤ filtration Q n

The products of exactly n generators are among the products of at most n of them.

theorem CliffordAlgebra.filtration_eq_iSup_pow {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (k : ℕ) : filtration Q k = ⨆ (i : { i : ℕ // i ≤ k }), (ι Q).range ^ ↑i

The comparison between the filtration and the submodule powers of LinearMap.range (ι Q): filtration Q k collects the products of at most k generators, so it is the supremum of the powers up to k. Compare CliffordAlgebra.evenOdd, the supremum of the powers whose exponent has a fixed parity.

theorem CliffordAlgebra.filtration_succ_eq_sup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (k : ℕ) : filtration Q (k + 1) = filtration Q k ⊔ (ι Q).range ^ (k + 1)

The successor step of the filtration adjoins the products of exactly k + 1 generators.

theorem CliffordAlgebra.iSup_filtration_eq_top {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ⨆ (k : ℕ), filtration Q k = ⊤

The filtration is exhaustive. Every element of the Clifford algebra is a combination of products of generators, so it lies in some step.

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

The degree-k + 1 leading-term map from the exterior power to the corresponding Clifford filtration quotient. A repeated generator becomes a lower-filtration term under the Clifford relation, so the product descends to an alternating map.

This is the CommRing-level half of the Layer 0 filtrationGradedEquiv target in the spin representations roadmap.

Equations

• CliffordAlgebra.filtrationLeadingTerm Q k = exteriorPower.alternatingMapLinearEquiv (CliffordAlgebra.filtrationLeadingTermAlternating✝ Q k)

@[simp]

theorem CliffordAlgebra.filtrationLeadingTerm_apply_ιMulti {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (k : ℕ) (v : Fin (k + 1) → M) : (filtrationLeadingTerm Q k) ((exteriorPower.ιMulti R (k + 1)) v) = Submodule.Quotient.mk ⟨(List.ofFn (⇑(ι Q) ∘ v)).prod, ⋯⟩

The leading-term map sends an exterior product to the class of the corresponding product of Clifford generators.

theorem CliffordAlgebra.filtrationLeadingTerm_surjective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (k : ℕ) : Function.Surjective ⇑(filtrationLeadingTerm Q k)

Every element of the degree-k + 1 Clifford filtration quotient is the leading term of an element of the degree-k + 1 exterior power.

theorem CliffordAlgebra.involute_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {k : ℕ} {x : CliffordAlgebra Q} (hx : x ∈ filtration Q k) : involute x ∈ filtration Q k

The grade involution preserves each step of the filtration: it multiplies a product of n generators by (-1) ^ n.

theorem CliffordAlgebra.reverse_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {k : ℕ} {x : CliffordAlgebra Q} (hx : x ∈ filtration Q k) : reverse x ∈ filtration Q k

Reversal preserves each step of the filtration: it reverses the list of generators.

theorem CliffordAlgebra.map_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {N : Type w} [AddCommGroup N] [Module R N] {Q' : QuadraticForm R N} (f : Q →qᵢ Q') {k : ℕ} {x : CliffordAlgebra Q} (hx : x ∈ filtration Q k) : (map f) x ∈ filtration Q' k

An isometry of quadratic forms respects the degree filtration: it takes a product of generators to a product of the same length.

theorem CliffordAlgebra.contractLeft_mem_filtration_succ {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) {k : ℕ} {x : CliffordAlgebra Q} (hx : x ∈ filtration Q (k + 1)) : (contractLeft d) x ∈ filtration Q k

Left contraction lowers every positive filtration step by one.

theorem CliffordAlgebra.contractLeft_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (d : Module.Dual R M) {k : ℕ} {x : CliffordAlgebra Q} (hx : x ∈ filtration Q k) : (contractLeft d) x ∈ filtration Q k

Left contraction preserves each filtration step.

theorem CliffordAlgebra.changeForm_prod_map_ι_sub_prod_map_ι_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (l : List M) {k : ℕ} : l.length ≤ k + 2 → (changeForm h) (List.map (⇑(ι Q)) l).prod - (List.map (⇑(ι Q')) l).prod ∈ filtration Q' k

Change of form has identity symbol, and its correction is even. Transporting a word of at most k + 2 generators along changeForm changes it only by terms of filtration degree at most k: the difference between the word in the ι Q and the same word in the ι Q' drops two steps. It corrects by left contractions, and each contraction removes a pair of generators, so a one-step bound would not be sharp. Mathlib's changeForm_ι_mul_ι is the first instance: a two-generator word is corrected by the scalar B m₁ m₂, which lies in filtration Q' 0.

Where changeForm_mem_filtration says changeForm is a filtered map, this says its associated graded map is the identity.

theorem CliffordAlgebra.changeForm_mem_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) {k : ℕ} {x : CliffordAlgebra Q} (hx : x ∈ filtration Q k) : (changeForm h) x ∈ filtration Q' k

Changing quadratic form by a bilinear form preserves each filtration step.

@[simp]

theorem CliffordAlgebra.changeFormEquiv_map_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (k : ℕ) : Submodule.map (↑(changeFormEquiv h)) (filtration Q k) = filtration Q' k

The change-form equivalence transports every Clifford filtration step exactly.

@[simp]

theorem CliffordAlgebra.changeForm_mem_filtration_iff {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q) (k : ℕ) (x : CliffordAlgebra Q) : (changeForm h) x ∈ filtration Q' k ↔ x ∈ filtration Q k

Membership in the filtration is invariant under the change-form equivalence. The statement uses changeForm, the simplifier's normal form for applying changeFormEquiv.

theorem CliffordAlgebra.fg_filtration {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Module.Finite R M] (k : ℕ) : (filtration Q k).FG

Every step of the filtration is a finitely generated module as soon as M is: the k-th step is generated by the products of at most k elements of a generating family of M.

theorem CliffordAlgebra.filtration_eq_top_of_finrank_le {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) {n : ℕ} (hV : Module.finrank K V ≤ n) : filtration Q n = ⊤

The filtration stops at the dimension. Over a field, every element of the Clifford algebra of a finite-dimensional space of dimension at most n is a combination of products of at most n generators: the exterior powers above the dimension vanish, so from degree n + 1 on the leading-term map has a trivial target and each step of the filtration equals the previous one.