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) : AlgHom R (CliffordAlgebra Q) (CliffordAlgebra (QuadraticForm.baseChange A Q))

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

Equations

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

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) : Eq (DFunLike.coe (ofBaseChangeAux A Q) (DFunLike.coe (ι Q) v)) (DFunLike.coe (ι (QuadraticForm.baseChange A Q)) (TensorProduct.tmul R 1 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) : AlgHom A (TensorProduct R A (CliffordAlgebra Q)) (CliffordAlgebra (QuadraticForm.baseChange A Q))

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

Equations

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

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) : Eq (DFunLike.coe (ofBaseChange A Q) (TensorProduct.tmul R z (DFunLike.coe (ι Q) v))) (DFunLike.coe (ι (QuadraticForm.baseChange A Q)) (TensorProduct.tmul R z v))

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) : Eq (DFunLike.coe (ofBaseChange A Q) (TensorProduct.tmul R z 1)) (DFunLike.coe (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) : AlgHom A (CliffordAlgebra (QuadraticForm.baseChange A Q)) (TensorProduct R A (CliffordAlgebra Q))

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

Equations

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

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) : Eq (DFunLike.coe (toBaseChange A Q) (DFunLike.coe (ι (QuadraticForm.baseChange A Q)) (TensorProduct.tmul R z v))) (TensorProduct.tmul R z (DFunLike.coe (ι 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) : Eq ((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)) : Eq (DFunLike.coe (toBaseChange A Q) (DFunLike.coe involute x)) (DFunLike.coe (TensorProduct.map LinearMap.id involute.toLinearMap) (DFunLike.coe (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) : Eq ((DFunLike.coe AlgHom.op (toBaseChange A Q)).comp reverseOp) ((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)).toAlgHom.comp ((Algebra.TensorProduct.map (AlgEquiv.toOpposite A A).toAlgHom 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)) : Eq (DFunLike.coe (toBaseChange A Q) (DFunLike.coe reverse x)) (DFunLike.coe (TensorProduct.map LinearMap.id reverse) (DFunLike.coe (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) : Eq ((toBaseChange A Q).comp (ofBaseChange A Q)) (AlgHom.id A (TensorProduct R A (CliffordAlgebra Q)))

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)) : Eq (DFunLike.coe (toBaseChange A Q) (DFunLike.coe (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) : Eq ((ofBaseChange A Q).comp (toBaseChange A Q)) (AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q)))

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)) : Eq (DFunLike.coe (ofBaseChange A Q) (DFunLike.coe (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) : AlgEquiv A (CliffordAlgebra (QuadraticForm.baseChange A Q)) (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

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

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)) : Eq (DFunLike.coe (equivBaseChange A Q).symm a) (DFunLike.coe (ofBaseChange A Q) a)

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)) : Eq (DFunLike.coe (equivBaseChange A Q) a) (DFunLike.coe (toBaseChange A Q) a)