# Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

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

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.

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.

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 : ) :
AlgHom.comp () CliffordAlgebra.involute = AlgHom.comp (Algebra.TensorProduct.map () CliffordAlgebra.involute) ()
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 (AlgHom.toLinearMap CliffordAlgebra.involute)) (↑() 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.comp (AlgHom.op ()) CliffordAlgebra.reverseOp = AlgHom.comp (↑()) (AlgHom.comp (Algebra.TensorProduct.map (↑()) CliffordAlgebra.reverseOp) ())

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 : ) :
= 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 : ) :
@[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 : ) :
↑() 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 = ↑() 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.

Instances For