Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

The base change of a clifford algebra #

In this file we show the isomorphism

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:

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

Equations
@[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) :

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

Equations
@[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) :

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

Equations
@[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

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

Auxiliary theorem used to prove toBaseChange_reverse without needing induction.

reverse acts only on the right of the tensor product.

@[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
@[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

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
@[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)) :
@[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)) :