The base change of a clifford algebra

In this file we show the isomorphism

• CliffordAlgebra.equivBaseChange A Q : CliffordAlgebra (Q.baseChange A) ≃ₐ[A] (A ⊗[R] CliffordAlgebra Q) with forward direction CliffordAlgebra.toBasechange A Q and reverse direction CliffordAlgebra.ofBasechange A Q.

This covers a more general case of the complexification of clifford algebras (as described in §2.2 of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf), where ℂ and ℝ are replaced by an R-algebra A (where 2 : R is invertible).

We show the additional results:

• CliffordAlgebra.toBasechange_ι: the effect of base-changing pure vectors.
• CliffordAlgebra.ofBasechange_tmul_ι: the effect of un-base-changing a tensor of a pure vectors.
• CliffordAlgebra.toBasechange_involute: the effect of base-changing an involution.
• CliffordAlgebra.toBasechange_reverse: the effect of base-changing a reversal.

noncomputable def CliffordAlgebra.ofBaseChangeAux {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : CliffordAlgebra Q →ₐ[R] CliffordAlgebra (QuadraticForm.baseChange A Q)

Auxiliary construction: note this is really just a heterobasic CliffordAlgebra.map.

Equations

• CliffordAlgebra.ofBaseChangeAux A Q = (CliffordAlgebra.lift Q) ⟨↑R (CliffordAlgebra.ι (QuadraticForm.baseChange A Q)) ∘ₗ (TensorProduct.mk R A V) 1, ⋯⟩

@[simp]

theorem CliffordAlgebra.ofBaseChangeAux_ι {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (v : V) : (ofBaseChangeAux A Q) ((ι Q) v) = (ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)

noncomputable def CliffordAlgebra.ofBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : TensorProduct R A (CliffordAlgebra Q) →ₐ[A] CliffordAlgebra (QuadraticForm.baseChange A Q)

Convert from the base-changed clifford algebra to the clifford algebra over a base-changed module.

Equations

• CliffordAlgebra.ofBaseChange A Q = Algebra.TensorProduct.lift (Algebra.ofId A (CliffordAlgebra (QuadraticForm.baseChange A Q))) (CliffordAlgebra.ofBaseChangeAux A Q) ⋯

@[simp]

theorem CliffordAlgebra.ofBaseChange_tmul_ι {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (z : A) (v : V) : (ofBaseChange A Q) (z ⊗ₜ[R] (ι Q) v) = (ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)

@[simp]

theorem CliffordAlgebra.ofBaseChange_tmul_one {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (z : A) : (ofBaseChange A Q) (z ⊗ₜ[R] 1) = (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z

noncomputable def CliffordAlgebra.toBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : CliffordAlgebra (QuadraticForm.baseChange A Q) →ₐ[A] TensorProduct R A (CliffordAlgebra Q)

Convert from the clifford algebra over a base-changed module to the base-changed clifford algebra.

Equations

• CliffordAlgebra.toBaseChange A Q = (CliffordAlgebra.lift (QuadraticForm.baseChange A Q)) ⟨TensorProduct.AlgebraTensorModule.map LinearMap.id (CliffordAlgebra.ι Q), ⋯⟩

@[simp]

theorem CliffordAlgebra.toBaseChange_ι {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (z : A) (v : V) : (toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)) = z ⊗ₜ[R] (ι Q) v

theorem CliffordAlgebra.toBaseChange_comp_involute {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : (toBaseChange A Q).comp involute = (Algebra.TensorProduct.map (AlgHom.id A A) involute).comp (toBaseChange A Q)

theorem CliffordAlgebra.toBaseChange_involute {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (x : CliffordAlgebra (QuadraticForm.baseChange A Q)) : (toBaseChange A Q) (involute x) = (TensorProduct.map LinearMap.id involute.toLinearMap) ((toBaseChange A Q) x)

The involution acts only on the right of the tensor product.

theorem CliffordAlgebra.toBaseChange_comp_reverseOp {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : (AlgHom.op (toBaseChange A Q)).comp reverseOp = (↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q))

Auxiliary theorem used to prove toBaseChange_reverse without needing induction.

theorem CliffordAlgebra.toBaseChange_reverse {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (x : CliffordAlgebra (QuadraticForm.baseChange A Q)) : (toBaseChange A Q) (reverse x) = (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)

reverse acts only on the right of the tensor product.

theorem CliffordAlgebra.toBaseChange_comp_ofBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : (toBaseChange A Q).comp (ofBaseChange A Q) = AlgHom.id A (TensorProduct R A (CliffordAlgebra Q))

@[simp]

theorem CliffordAlgebra.toBaseChange_ofBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (x : TensorProduct R A (CliffordAlgebra Q)) : (toBaseChange A Q) ((ofBaseChange A Q) x) = x

theorem CliffordAlgebra.ofBaseChange_comp_toBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : (ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q))

@[simp]

theorem CliffordAlgebra.ofBaseChange_toBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (x : CliffordAlgebra (QuadraticForm.baseChange A Q)) : (ofBaseChange A Q) ((toBaseChange A Q) x) = x

noncomputable def CliffordAlgebra.equivBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) : CliffordAlgebra (QuadraticForm.baseChange A Q) ≃ₐ[A] TensorProduct R A (CliffordAlgebra Q)

Base-changing the vector space of a clifford algebra is isomorphic as an A-algebra to base-changing the clifford algebra itself; <|Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R Cℓ(V, Q)<|.

This is CliffordAlgebra.toBaseChange and CliffordAlgebra.ofBaseChange as an equivalence.

Equations

• CliffordAlgebra.equivBaseChange A Q = AlgEquiv.ofAlgHom (CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.ofBaseChange A Q) ⋯ ⋯

@[simp]

theorem CliffordAlgebra.equivBaseChange_symm_apply {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (a : TensorProduct R A (CliffordAlgebra Q)) : (equivBaseChange A Q).symm a = (ofBaseChange A Q) a

@[simp]

theorem CliffordAlgebra.equivBaseChange_apply {R : Type u_1} (A : Type u_2) {V : Type u_3} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (a : CliffordAlgebra (QuadraticForm.baseChange A Q)) : (equivBaseChange A Q) a = (toBaseChange A Q) a