Documentation

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Clifford Algebras #

We construct the Clifford algebra of a module M over a commutative ring R, equipped with a quadratic form Q.

Notation #

The Clifford algebra of the R-module M equipped with a quadratic form Q is an R-algebra denoted CliffordAlgebra Q.

Given a linear morphism f : M → A from a module M to another R-algebra A, such that cond : ∀ m, f m * f m = algebraMap _ _ (Q m), there is a (unique) lift of f to an R-algebra morphism from CliffordAlgebra Q to A, which is denoted CliffordAlgebra.lift Q f cond.

The canonical linear map M → CliffordAlgebra Q is denoted CliffordAlgebra.ι Q.

Theorems #

The main theorems proved ensure that CliffordAlgebra Q satisfies the universal property of the Clifford algebra.

  1. ι_comp_lift is the fact that the composition of ι Q with lift Q f cond agrees with f.
  2. lift_unique ensures the uniqueness of lift Q f cond with respect to 1.

Implementation details #

The Clifford algebra of M is constructed as a quotient of the tensor algebra, as follows.

  1. We define a relation CliffordAlgebra.Rel Q on TensorAlgebra R M. This is the smallest relation which identifies squares of elements of M with Q m.
  2. The Clifford algebra is the quotient of the tensor algebra by this relation.

This file is almost identical to Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean.

source
inductive CliffordAlgebra.Rel {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
TensorAlgebra R M → TensorAlgebra R M → Prop

Rel relates each ι m * ι m, for m : M, with Q m.

The Clifford algebra of M is defined as the quotient modulo this relation.

Instances For
    source
    def CliffordAlgebra {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
    Type (max u_2 u_1)

    The Clifford algebra of an R-module M equipped with a quadratic_form Q.

    Equations
    Instances For
      source
      instance CliffordAlgebra.instInhabited {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
      Inhabited (CliffordAlgebra Q)
      Equations
      source
      instance CliffordAlgebra.instRing {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
      Ring (CliffordAlgebra Q)
      Equations
      source
      @[instance 900]
      instance CliffordAlgebra.instAlgebra' {R : Type u_3} {A : Type u_4} {M : Type u_5} [CommSemiring R] [AddCommGroup M] [CommRing A] [Algebra R A] [Module R M] [Module A M] (Q : QuadraticForm A M) [IsScalarTower R A M] :
      Algebra R (CliffordAlgebra Q)
      Equations
      source
      instance CliffordAlgebra.instAlgebra {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
      Algebra R (CliffordAlgebra Q)
      Equations
      source
      instance CliffordAlgebra.instSMulCommClass {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [CommSemiring R] [CommSemiring S] [AddCommGroup M] [CommRing A] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] (Q : QuadraticForm A M) [IsScalarTower R A M] [IsScalarTower S A M] :
      SMulCommClass R S (CliffordAlgebra Q)
      Equations
      • ⋯ = ⋯
      source
      instance CliffordAlgebra.instIsScalarTower {R : Type u_3} {S : Type u_4} {A : Type u_5} {M : Type u_6} [CommSemiring R] [CommSemiring S] [AddCommGroup M] [CommRing A] [SMul R S] [Algebra R A] [Algebra S A] [Module R M] [Module S M] [Module A M] [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S A] (Q : QuadraticForm A M) :
      IsScalarTower R S (CliffordAlgebra Q)
      Equations
      • ⋯ = ⋯
      source
      def CliffordAlgebra.ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) :
      M →ₗ[R] CliffordAlgebra Q

      The canonical linear map M →ₗ[R] CliffordAlgebra Q.

      Equations
      Instances For
        source
        @[simp]
        theorem CliffordAlgebra.ι_sq_scalar {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (m : M) :
        (CliffordAlgebra.ι Q) m * (CliffordAlgebra.ι Q) m = (algebraMap R (CliffordAlgebra Q)) (Q m)

        As well as being linear, ι Q squares to the quadratic form

        source
        @[simp]
        theorem CliffordAlgebra.comp_ι_sq_scalar {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type u_3} [Semiring A] [Algebra R A] (g : CliffordAlgebra Q →ₐ[R] A) (m : M) :
        g ((CliffordAlgebra.ι Q) m) * g ((CliffordAlgebra.ι Q) m) = (algebraMap R A) (Q m)
        source
        @[simp]
        theorem CliffordAlgebra.lift_symm_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type u_3} [Semiring A] [Algebra R A] (F : CliffordAlgebra Q →ₐ[R] A) :
        (CliffordAlgebra.lift Q).symm F = ⟨F.toLinearMap ∘ₗ CliffordAlgebra.ι Q, ⋯⟩
        source
        def CliffordAlgebra.lift {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) {A : Type u_3} [Semiring A] [Algebra R A] :
        { f : M →ₗ[R] A // ∀ (m : M), f m * f m = (algebraMap R A) (Q m) } ≃ (CliffordAlgebra Q →ₐ[R] A)

        Given a linear map f : M →ₗ[R] A into an R-algebra A, which satisfies the condition: cond : ∀ m : M, f m * f m = Q(m), this is the canonical lift of f to a morphism of R-algebras from CliffordAlgebra Q to A.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CliffordAlgebra.ι_comp_lift {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type u_3} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)) :
          ((CliffordAlgebra.lift Q) ⟨f, cond⟩).toLinearMap ∘ₗ CliffordAlgebra.ι Q = f
          source
          @[simp]
          theorem CliffordAlgebra.lift_ι_apply {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type u_3} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)) (x : M) :
          ((CliffordAlgebra.lift Q) ⟨f, cond⟩) ((CliffordAlgebra.ι Q) x) = f x
          source
          @[simp]
          theorem CliffordAlgebra.lift_unique {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type u_3} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)) (g : CliffordAlgebra Q →ₐ[R] A) :
          g.toLinearMap ∘ₗ CliffordAlgebra.ι Q = f ↔ g = (CliffordAlgebra.lift Q) ⟨f, cond⟩
          source
          @[simp]
          theorem CliffordAlgebra.lift_comp_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type u_3} [Semiring A] [Algebra R A] (g : CliffordAlgebra Q →ₐ[R] A) :
          (CliffordAlgebra.lift Q) ⟨g.toLinearMap ∘ₗ CliffordAlgebra.ι Q, ⋯⟩ = g
          source
          theorem CliffordAlgebra.hom_ext {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type u_4} [Semiring A] [Algebra R A] {f : CliffordAlgebra Q →ₐ[R] A} {g : CliffordAlgebra Q →ₐ[R] A} :
          f.toLinearMap ∘ₗ CliffordAlgebra.ι Q = g.toLinearMap ∘ₗ CliffordAlgebra.ι Q → f = g

          See note [partially-applied ext lemmas].

          source
          theorem CliffordAlgebra.induction {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {C : CliffordAlgebra Q → Prop} (algebraMap : ∀ (r : R), C ((_root_.algebraMap R (CliffordAlgebra Q)) r)) (ι : ∀ (x : M), C ((CliffordAlgebra.ι Q) x)) (mul : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a * b)) (add : ∀ (a b : CliffordAlgebra Q), C a → C b → C (a + b)) (a : CliffordAlgebra Q) :
          C a

          If C holds for the algebraMap of r : R into CliffordAlgebra Q, the ι of x : M, and is preserved under addition and muliplication, then it holds for all of CliffordAlgebra Q.

          See also the stronger CliffordAlgebra.left_induction and CliffordAlgebra.right_induction.

          source
          theorem CliffordAlgebra.mul_add_swap_eq_polar_of_forall_mul_self_eq {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type u_4} [Ring A] [Algebra R A] (f : M →ₗ[R] A) (hf : ∀ (x : M), f x * f x = (algebraMap R A) (Q x)) (a : M) (b : M) :
          f a * f b + f b * f a = (algebraMap R A) (QuadraticMap.polar (⇑Q) a b)
          source
          theorem CliffordAlgebra.forall_mul_self_eq_iff {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type u_4} [Ring A] [Algebra R A] (h2 : IsUnit 2) (f : M →ₗ[R] A) :
          (∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔ (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f = LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)

          An alternative way to provide the argument to CliffordAlgebra.lift when 2 is invertible.

          To show a function squares to the quadratic form, it suffices to show that f x * f y + f y * f x = algebraMap _ _ (polar Q x y)

          source
          theorem CliffordAlgebra.ι_mul_ι_add_swap {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a : M) (b : M) :
          (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b + (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a = (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b)

          The symmetric product of vectors is a scalar

          source
          theorem CliffordAlgebra.ι_mul_ι_comm {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a : M) (b : M) :
          (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b = (algebraMap R (CliffordAlgebra Q)) (QuadraticMap.polar (⇑Q) a b) - (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a
          source
          @[simp]
          theorem CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {a : M} {b : M} (h : QuadraticMap.IsOrtho Q a b) :
          (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b + (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a = 0
          source
          theorem CliffordAlgebra.ι_mul_ι_comm_of_isOrtho {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {a : M} {b : M} (h : QuadraticMap.IsOrtho Q a b) :
          (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b = -((CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a)
          source
          theorem CliffordAlgebra.mul_ι_mul_ι_of_isOrtho {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : CliffordAlgebra Q) {a : M} {b : M} (h : QuadraticMap.IsOrtho Q a b) :
          x * (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b = -(x * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a)
          source
          theorem CliffordAlgebra.ι_mul_ι_mul_of_isOrtho {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : CliffordAlgebra Q) {a : M} {b : M} (h : QuadraticMap.IsOrtho Q a b) :
          (CliffordAlgebra.ι Q) a * ((CliffordAlgebra.ι Q) b * x) = -((CliffordAlgebra.ι Q) b * ((CliffordAlgebra.ι Q) a * x))
          source
          theorem CliffordAlgebra.ι_mul_ι_mul_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (a : M) (b : M) :
          (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a = (CliffordAlgebra.ι Q) (QuadraticMap.polar (⇑Q) a b • a - Q a • b)

          $aba$ is a vector.

          source
          @[simp]
          theorem CliffordAlgebra.ι_range_map_lift {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {A : Type u_3} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)) :
          Submodule.map ((CliffordAlgebra.lift Q) ⟨f, cond⟩).toLinearMap (LinearMap.range (CliffordAlgebra.ι Q)) = LinearMap.range f
          source
          def CliffordAlgebra.map {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) :
          CliffordAlgebra Q₁ →ₐ[R] CliffordAlgebra Q₂

          Any linear map that preserves the quadratic form lifts to an AlgHom between algebras.

          See CliffordAlgebra.equivOfIsometry for the case when f is a QuadraticForm.IsometryEquiv.

          Equations
          Instances For
            source
            @[simp]
            theorem CliffordAlgebra.map_comp_ι {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) :
            (CliffordAlgebra.map f).toLinearMap ∘ₗ CliffordAlgebra.ι Q₁ = CliffordAlgebra.ι Q₂ ∘ₗ f.toLinearMap
            source
            @[simp]
            theorem CliffordAlgebra.map_apply_ι {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (m : M₁) :
            (CliffordAlgebra.map f) ((CliffordAlgebra.ι Q₁) m) = (CliffordAlgebra.ι Q₂) (f m)
            source
            @[simp]
            theorem CliffordAlgebra.map_id {R : Type u_1} [CommRing R] {M₁ : Type u_4} [AddCommGroup M₁] [Module R M₁] (Q₁ : QuadraticForm R M₁) :
            CliffordAlgebra.map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁)
            source
            @[simp]
            theorem CliffordAlgebra.map_comp_map {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} (f : Q₂ →qᵢ Q₃) (g : Q₁ →qᵢ Q₂) :
            (CliffordAlgebra.map f).comp (CliffordAlgebra.map g) = CliffordAlgebra.map (f.comp g)
            source
            @[simp]
            theorem CliffordAlgebra.ι_range_map_map {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) :
            Submodule.map (CliffordAlgebra.map f).toLinearMap (LinearMap.range (CliffordAlgebra.ι Q₁)) = Submodule.map (CliffordAlgebra.ι Q₂) (LinearMap.range f.toLinearMap)
            source
            theorem CliffordAlgebra.leftInverse_map_of_leftInverse {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (g : Q₂ →qᵢ Q₁) (h : Function.LeftInverse ⇑g ⇑f) :
            Function.LeftInverse ⇑(CliffordAlgebra.map g) ⇑(CliffordAlgebra.map f)

            If f is a linear map from M₁ to M₂ that preserves the quadratic forms, and if it has a linear retraction g that also preserves the quadratic forms, then CliffordAlgebra.map g is a retraction of CliffordAlgebra.map f.

            source
            theorem CliffordAlgebra.map_surjective {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (hf : Function.Surjective ⇑f) :
            Function.Surjective ⇑(CliffordAlgebra.map f)

            If a linear map preserves the quadratic forms and is surjective, then the algebra maps it induces between Clifford algebras is also surjective.

            source
            @[simp]
            theorem CliffordAlgebra.equivOfIsometry_apply {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) (a : CliffordAlgebra Q₁) :
            (CliffordAlgebra.equivOfIsometry e) a = (CliffordAlgebra.map e.toIsometry) a
            source
            def CliffordAlgebra.equivOfIsometry {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) :
            CliffordAlgebra Q₁ ≃ₐ[R] CliffordAlgebra Q₂

            Two CliffordAlgebras are equivalent as algebras if their quadratic forms are equivalent.

            Equations
            Instances For
              source
              @[simp]
              theorem CliffordAlgebra.equivOfIsometry_symm {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) :
              (CliffordAlgebra.equivOfIsometry e).symm = CliffordAlgebra.equivOfIsometry e.symm
              source
              @[simp]
              theorem CliffordAlgebra.equivOfIsometry_trans {R : Type u_1} [CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} (e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂) (e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃) :
              (CliffordAlgebra.equivOfIsometry e₁₂).trans (CliffordAlgebra.equivOfIsometry e₂₃) = CliffordAlgebra.equivOfIsometry (e₁₂.trans e₂₃)
              source
              @[simp]
              theorem CliffordAlgebra.equivOfIsometry_refl {R : Type u_1} [CommRing R] {M₁ : Type u_4} [AddCommGroup M₁] [Module R M₁] {Q₁ : QuadraticForm R M₁} :
              CliffordAlgebra.equivOfIsometry (QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl
              source
              def TensorAlgebra.toClifford {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} :
              TensorAlgebra R M →ₐ[R] CliffordAlgebra Q

              The canonical image of the TensorAlgebra in the CliffordAlgebra, which maps TensorAlgebra.ι R x to CliffordAlgebra.ι Q x.

              Equations
              Instances For
                source
                @[simp]
                theorem TensorAlgebra.toClifford_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (m : M) :
                TensorAlgebra.toClifford ((TensorAlgebra.ι R) m) = (CliffordAlgebra.ι Q) m