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

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

        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