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).

• 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} [] [] [] [Algebra R A] [Module R V] [] (Q : ) :

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

Equations
• = R ∘ₗ () 1,
Instances For
@[simp]
theorem CliffordAlgebra.ofBaseChangeAux_ι {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (v : V) :
( v) = (1 ⊗ₜ[R] v)
noncomputable def CliffordAlgebra.ofBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) :

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

Equations
Instances For
@[simp]
theorem CliffordAlgebra.ofBaseChange_tmul_ι {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (z : A) (v : V) :
(z ⊗ₜ[R] v) = (z ⊗ₜ[R] v)
@[simp]
theorem CliffordAlgebra.ofBaseChange_tmul_one {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (z : A) :
(z ⊗ₜ[R] 1) = () z
noncomputable def CliffordAlgebra.toBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) :

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

Equations
Instances For
@[simp]
theorem CliffordAlgebra.toBaseChange_ι {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (z : A) (v : V) :
( (z ⊗ₜ[R] v)) = z ⊗ₜ[R] v
theorem CliffordAlgebra.toBaseChange_comp_involute {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) :
.comp CliffordAlgebra.involute = (Algebra.TensorProduct.map () CliffordAlgebra.involute).comp
theorem CliffordAlgebra.toBaseChange_involute {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (x : ) :
(CliffordAlgebra.involute x) = (TensorProduct.map LinearMap.id CliffordAlgebra.involute.toLinearMap) ( 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} [] [] [] [Algebra R A] [Module R V] [] (Q : ) :
(AlgHom.op ).comp CliffordAlgebra.reverseOp = (()).comp ((Algebra.TensorProduct.map (()) CliffordAlgebra.reverseOp).comp )

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} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (x : ) :
(CliffordAlgebra.reverse x) = (TensorProduct.map LinearMap.id CliffordAlgebra.reverse) ( 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} [] [] [] [Algebra R A] [Module R V] [] (Q : ) :
.comp = AlgHom.id A ()
@[simp]
theorem CliffordAlgebra.toBaseChange_ofBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (x : ) :
( x) = x
theorem CliffordAlgebra.ofBaseChange_comp_toBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) :
.comp =
@[simp]
theorem CliffordAlgebra.ofBaseChange_toBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (x : ) :
( x) = x
@[simp]
theorem CliffordAlgebra.equivBaseChange_symm_apply {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (a : ) :
.symm a = a
@[simp]
theorem CliffordAlgebra.equivBaseChange_apply {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (Q : ) (a : ) :
= a
noncomputable def CliffordAlgebra.equivBaseChange {R : Type u_1} (A : Type u_2) {V : Type u_3} [] [] [] [Algebra R A] [Module R V] [] (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
Instances For