Theorems · Definition · linear algebra

CliffordAlgebra.equivBaseChange

{R : Type u_1} →
  (A : Type u_2) →
    {V : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R V] →
                [inst_5 : Invertible 2] →
                  (Q : QuadraticForm R V) →
                    CliffordAlgebra (QuadraticForm.baseChange A Q) ≃ₐ[A] TensorProduct R A (CliffordAlgebra 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.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Cited by

2 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAddCommGroupAlgebraModuleInvertible