Clifford involutions, the even part, and extension of scalars

This file records the structural properties of Mathlib's CliffordAlgebra.ofBaseChangeAux, the canonical map from a Clifford algebra into the Clifford algebra after extension of scalars: it commutes with the grade involution and with Clifford conjugation, and it preserves the even subalgebra. These are the compatibilities needed to transport twisted-conjugation actions and the Lipschitz, Pin, and Spin subgroups along scalar extensions.

Main results

• CliffordAlgebra.ofBaseChangeAux_involute proves naturality of the grade involution.
• CliffordAlgebra.ofBaseChangeAux_reverse proves naturality of Clifford reversal.
• CliffordAlgebra.ofBaseChangeAux_star proves naturality of Clifford conjugation.
• CliffordAlgebra.ofBaseChangeAux_mem_even proves preservation of the even subalgebra.
• CliffordAlgebra.ofBaseChangeAux_injective proves injectivity for faithful flat extensions.
• CliffordAlgebra.ofBaseChangeAux_baseChange identifies direct and successive scalar extension.

@[simp]

theorem CliffordAlgebra.ofBaseChangeAux_involute {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : CliffordAlgebra Q) : (ofBaseChangeAux A Q) (involute x) = involute ((ofBaseChangeAux A Q) x)

The canonical map to the Clifford algebra after extension of scalars commutes with the grade involution.

@[simp]

theorem CliffordAlgebra.ofBaseChangeAux_reverse {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : CliffordAlgebra Q) : (ofBaseChangeAux A Q) (reverse x) = reverse ((ofBaseChangeAux A Q) x)

The canonical map to the Clifford algebra after extension of scalars commutes with Clifford reversal.

@[simp]

theorem CliffordAlgebra.ofBaseChangeAux_star {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : CliffordAlgebra Q) : (ofBaseChangeAux A Q) (star x) = star ((ofBaseChangeAux A Q) x)

The canonical map to the Clifford algebra after extension of scalars commutes with Clifford conjugation.

theorem CliffordAlgebra.ofBaseChangeAux_mem_even {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) {x : CliffordAlgebra Q} (hx : x ∈ even Q) : (ofBaseChangeAux A Q) x ∈ even (QuadraticForm.baseChange A Q)

The canonical map to the Clifford algebra after extension of scalars sends even elements to even elements.

@[simp]

theorem CliffordAlgebra.toBaseChange_ofBaseChangeAux {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] (Q : QuadraticForm R M) (x : CliffordAlgebra Q) : (toBaseChange A Q) ((ofBaseChangeAux A Q) x) = 1 ⊗ₜ[R] x

Under the identification Cℓ(A ⊗ M) ≃ A ⊗ Cℓ(M) of CliffordAlgebra.toBaseChange, the canonical map to the Clifford algebra after extension of scalars sends x to 1 ⊗ x.

theorem CliffordAlgebra.ofBaseChangeAux_injective {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] [FaithfulSMul R A] (Q : QuadraticForm R M) [Module.Flat R (CliffordAlgebra Q)] : Function.Injective ⇑(ofBaseChangeAux A Q)

The canonical map to the Clifford algebra after extension of scalars is injective when the extension is faithful and the Clifford algebra is flat; in particular, for every extension of fields.

@[simp]

theorem CliffordAlgebra.ofBaseChangeAux_baseChange {R : Type u} {A : Type v} {M : Type w} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Invertible 2] {B : Type x} [CommRing B] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (Q : QuadraticForm R M) (z : CliffordAlgebra Q) : (map Q.baseChangeBaseChange.toIsometry) ((ofBaseChangeAux B Q) z) = (ofBaseChangeAux B (QuadraticForm.baseChange A Q)) ((ofBaseChangeAux A Q) z)

Transporting a direct scalar extension of a Clifford element along the canonical scalar-tower isometry agrees with extending the element successively.