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
Instances For

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

    Equations
    Instances For
      @[simp]

      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} [CommRing R] [CommRing A] [AddCommGroup V] [Algebra R A] [Module R V] [Invertible 2] (Q : QuadraticForm R V) (z : A) (v : 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) :
        (CliffordAlgebra.toBaseChange A Q).comp CliffordAlgebra.involute = (Algebra.TensorProduct.map (AlgHom.id A A) CliffordAlgebra.involute).comp (CliffordAlgebra.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)) :
        (CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.involute x) = (TensorProduct.map LinearMap.id CliffordAlgebra.involute.toLinearMap) ((CliffordAlgebra.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 (CliffordAlgebra.toBaseChange A Q)).comp CliffordAlgebra.reverseOp = (↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) CliffordAlgebra.reverseOp).comp (CliffordAlgebra.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)) :
        (CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.reverse x) = (TensorProduct.map LinearMap.id CliffordAlgebra.reverse) ((CliffordAlgebra.toBaseChange A Q) x)

        reverse acts only on the right of the tensor product.

        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