An odd linear automorphism of a Clifford algebra

The two halves evenOdd Q 0 and evenOdd Q 1 of the ℤ/2-grading of a Clifford algebra are in general only submodules, with nothing relating their sizes. They become isomorphic as soon as some odd operator on CliffordAlgebra Q is invertible, because an odd operator carries each half into the other.

The odd operator to use is already in Mathlib: CliffordAlgebra.changeFormAux Q B e, the difference

x ↦ ι Q e * x - (B e)⌋x

of left Clifford multiplication by a vector — which is exterior multiplication only in the special case Q = 0, since in general it squares to Q e rather than to 0 — and contraction against the functional B e. Mathlib introduces it to build CliffordAlgebra.changeForm and proves there that it squares to the scalar Q e - B e e (CliffordAlgebra.changeFormAux_changeFormAux): expanding the square leaves the two cross terms ι Q e * ((B e)⌋x) and (B e)⌋(ι Q e * x), and CliffordAlgebra.contractLeft_ι_mul rewrites the second as B e e • x - ι Q e * ((B e)⌋x), whose second term cancels the first cross term while B e e • x survives; multiplication contributes Q e • x by the Clifford relation and the contraction squares to 0.

What Mathlib does not record is that the operator is odd, both of its summands being odd (CliffordAlgebra.map_evenOdd_changeFormAux_le). So whenever Q e - B e e is a unit the operator is a linear automorphism (CliffordAlgebra.paritySwapEquiv) exchanging the two halves of the grading.

Both degenerate choices are useful. Taking B = 0 recovers multiplication by an anisotropic vector, the classical reason a nondegenerate Clifford algebra has equidimensional halves; taking Q = 0 — the exterior algebra, where no vector is anisotropic — keeps exterior multiplication by e, which on its own now squares to 0, and has the contraction complement it: the combined operator squares to Q e - B e e = -B e e, a unit as soon as B e does not annihilate e. That second case is the one that was missing: it is what makes the two half-spin summands ⋀ᵉᵛᵉⁿ W and ⋀ᵒᵈᵈ W of a spinor module equidimensional.

Over a field the hypothesis is never an obstruction: a nonzero vector space always carries such a pair (QuadraticMap.exists_sub_bilinForm_eq_one), since a nonzero vector is not annihilated by every functional, and a rank-one bilinear form built from such a functional turns Q e - B e e into 1. Hence CliffordAlgebra.nonempty_evenOddEquivAddOne: over a field, the two halves of the grading of the Clifford algebra of a nonzero space are isomorphic, for every quadratic form. The dimension count that follows is CliffordAlgebra.finrank_evenOdd in TauCeti/LinearAlgebra/CliffordAlgebra/Dimension.lean.

Main definitions

• CliffordAlgebra.paritySwapEquiv: CliffordAlgebra.changeFormAux as a linear automorphism, when Q e - B e e is a unit.
• CliffordAlgebra.evenOddEquivAddOne: the induced isomorphism evenOdd Q i ≃ₗ evenOdd Q (i + 1).

Main results

• CliffordAlgebra.map_evenOdd_changeFormAux_le: the operator is odd.
• CliffordAlgebra.map_evenOdd_paritySwapEquiv: it carries evenOdd Q i onto evenOdd Q (i + 1).
• QuadraticMap.exists_sub_bilinForm_eq_one: over a field, a nonzero vector space carries a vector and a bilinear form with Q e - B e e = 1.
• CliffordAlgebra.nonempty_evenOddEquivAddOne: over a field, the two halves of the grading of the Clifford algebra of a nonzero space are isomorphic.

References

• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II, for the exterior multiplication and contraction operators and the Clifford relation between them.
• Clifford algebras, Pin and Spin, and spin representations roadmap, Layer 5, "The half-spin representation of 𝔰𝔬(2l) has dimension 2^{l-1}", whose dimension count this supplies.

theorem CliffordAlgebra.map_evenOdd_changeFormAux_le {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (B : LinearMap.BilinForm R M) (e : M) (i : ZMod 2) : Submodule.map ((changeFormAux Q B) e) (evenOdd Q i) ≤ evenOdd Q (i + 1)

The parity-swapping operator is odd: CliffordAlgebra.changeFormAux carries evenOdd Q i into evenOdd Q (i + 1), because both of its summands do — multiplication by a vector by the grading, contraction by CliffordAlgebra.contractLeft_mem_evenOdd.

noncomputable def CliffordAlgebra.paritySwapEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {B : LinearMap.BilinForm R M} {e : M} (h : IsUnit (Q e - (B e) e)) : CliffordAlgebra Q ≃ₗ[R] CliffordAlgebra Q

The parity-swapping automorphism: CliffordAlgebra.changeFormAux Q B e read as a linear automorphism, for a vector and a bilinear form whose scalar Q e - B e e is a unit. The inverse is the same operator rescaled by the inverse of that unit, since the operator squares to it (CliffordAlgebra.changeFormAux_changeFormAux).

Equations

• CliffordAlgebra.paritySwapEquiv h = LinearEquiv.ofLinearMap ((CliffordAlgebra.changeFormAux Q B) e) (↑h.unit⁻¹ • (CliffordAlgebra.changeFormAux Q B) e) ⋯ ⋯

@[simp]

theorem CliffordAlgebra.paritySwapEquiv_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {B : LinearMap.BilinForm R M} {e : M} (h : IsUnit (Q e - (B e) e)) (x : CliffordAlgebra Q) : (paritySwapEquiv h) x = ((changeFormAux Q B) e) x

The parity-swapping automorphism is the operator it is built from.

theorem CliffordAlgebra.paritySwapEquiv_toLinearMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {B : LinearMap.BilinForm R M} {e : M} (h : IsUnit (Q e - (B e) e)) : ↑(paritySwapEquiv h) = (changeFormAux Q B) e

The parity-swapping automorphism is the operator it is built from, as linear maps: the bridge that lets a statement about CliffordAlgebra.changeFormAux be read off one about CliffordAlgebra.paritySwapEquiv, and conversely.

@[simp]

theorem CliffordAlgebra.paritySwapEquiv_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {B : LinearMap.BilinForm R M} {e : M} (h : IsUnit (Q e - (B e) e)) (x : CliffordAlgebra Q) : (paritySwapEquiv h).symm x = ↑h.unit⁻¹ • ((changeFormAux Q B) e) x

The inverse of CliffordAlgebra.paritySwapEquiv is the same operator rescaled by the inverse of the unit it squares to.

@[simp]

theorem CliffordAlgebra.map_evenOdd_paritySwapEquiv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {B : LinearMap.BilinForm R M} {e : M} (h : IsUnit (Q e - (B e) e)) (i : ZMod 2) : Submodule.map (↑(paritySwapEquiv h)) (evenOdd Q i) = evenOdd Q (i + 1)

The parity-swapping automorphism exchanges the two halves of the grading. The inclusion ≤ is oddness; the reverse holds because the preimage of y is a scalar multiple of changeFormAux Q B e y, which lies in evenOdd Q (i + 1 + 1) = evenOdd Q i.

noncomputable def CliffordAlgebra.evenOddEquivAddOne {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {B : LinearMap.BilinForm R M} {e : M} (h : IsUnit (Q e - (B e) e)) (i : ZMod 2) : ↥(evenOdd Q i) ≃ₗ[R] ↥(evenOdd Q (i + 1))

The two halves of the ℤ/2-grading are isomorphic, for a vector and a bilinear form whose scalar Q e - B e e is a unit: the parity-swapping automorphism restricts to an isomorphism between them.

Equations

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

@[simp]

theorem CliffordAlgebra.coe_evenOddEquivAddOne_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {B : LinearMap.BilinForm R M} {e : M} (h : IsUnit (Q e - (B e) e)) (i : ZMod 2) (x : ↥(evenOdd Q i)) : ↑((evenOddEquivAddOne h i) x) = ((changeFormAux Q B) e) ↑x

The isomorphism between the two halves of the grading is the parity-swapping operator, read inside the Clifford algebra.

@[simp]

theorem CliffordAlgebra.coe_evenOddEquivAddOne_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {B : LinearMap.BilinForm R M} {e : M} (h : IsUnit (Q e - (B e) e)) (i : ZMod 2) (y : ↥(evenOdd Q (i + 1))) : ↑((evenOddEquivAddOne h i).symm y) = ↑h.unit⁻¹ • ((changeFormAux Q B) e) ↑y

The inverse of the isomorphism between the two halves of the grading is the parity-swapping operator rescaled by the inverse of the unit it squares to, read inside the Clifford algebra.

theorem QuadraticMap.exists_sub_bilinForm_eq_one {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] (Q : QuadraticForm K V) : ∃ (e : V) (B : LinearMap.BilinForm K V), Q e - (B e) e = 1

A nonzero vector space carries a parity-swapping pair, for every quadratic form. Choose a nonzero vector e and a functional f with f e = 1; the rank-one bilinear form B = f ⊗ (Q e - 1) • f then has B e e = Q e - 1.

This is what frees CliffordAlgebra.evenOddEquivAddOne from any hypothesis on Q: the classical choice B = 0 needs an anisotropic vector, which an exterior algebra has none of, while here the contraction supplies the missing unit.

theorem CliffordAlgebra.nonempty_evenOddEquivAddOne {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [Nontrivial V] (Q : QuadraticForm K V) (i : ZMod 2) : Nonempty (↥(evenOdd Q i) ≃ₗ[K] ↥(evenOdd Q (i + 1)))

Over a field the two halves of the ℤ/2-grading of the Clifford algebra of a nonzero space are isomorphic, for every quadratic form — in particular for the zero form, where the algebra is the exterior algebra and the halves are the even and the odd exterior powers.

The isomorphism is not canonical: it depends on the parity-swapping pair chosen by QuadraticMap.exists_sub_bilinForm_eq_one, so it is produced as a Nonempty.