Contraction against the ℤ/2-grading

Mathlib's CliffordAlgebra.contractLeft lowers the degree of a multivector by one, so it exchanges the two halves of the ℤ/2-grading. Mathlib records neither half of that sentence: involute interacts with products (involute is an algebra homomorphism) and with the grading, but never with a contraction, and evenOdd is never related to contractLeft at all.

This file proves both. That a contraction carries evenOdd Q i into evenOdd Q (i + 1) is the grading statement itself, and it is what makes an annihilation operator odd; anticommutation with the grade involution is its operator shadow, and is what makes the grade involution usable as an even operator alongside exterior multiplication and contraction — for instance because an anisotropic vector orthogonal to a polarization acts on a spinor module by its scalar coordinate times the grade involution.

The degree bookkeeping is in ZMod 2, where lowering and raising the degree by one are the same map, so evenOdd Q (i + 1) and evenOdd Q (i - 1) are the same submodule; the statement below names the first.

The parity statement is proved by induction over the grading; its base case is read off by CliffordAlgebra.exists_algebraMap_of_mem_range_ι_pow_zero and CliffordAlgebra.exists_ι_of_mem_range_ι_pow_one, which are general facts about the grading and live with it.

Main results

• CliffordAlgebra.contractLeft_mem_evenOdd: contraction shifts the parity.
• CliffordAlgebra.involute_contractLeft: involute (d ⌋ x) = -(d ⌋ involute x).

References

• D. Grinberg, The Clifford algebra and the Chevalley map, for the contraction operators themselves.

@[simp]

theorem CliffordAlgebra.involute_contractLeft {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) (x : CliffordAlgebra Q) : involute ((contractLeft d) x) = -(contractLeft d) (involute x)

The grade involution anticommutes with contraction. Contracting against a linear functional lowers the degree by one, hence swaps the even and odd parts of the Clifford algebra, so it anticommutes with the operator that is +1 on the even part and -1 on the odd part.

theorem CliffordAlgebra.contractLeft_mem_evenOdd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (d : Module.Dual R M) {i : ZMod 2} {x : CliffordAlgebra Q} (hx : x ∈ evenOdd Q i) : (contractLeft d) x ∈ evenOdd Q (i + 1)

Contraction shifts the parity. Contracting against a linear functional lowers the degree of a multivector by one, so it carries the i-th half of the ℤ/2-grading into the other one.