3.2. The universal property🔗

The universal property of the Clifford algebra Cl(Q) states that if A is a unital, associative R-algebra, then any linear map f : M → A such that f(m) ^ 2 = Q(m)1 factors as a composition of the Clifford map ι : M → Cl(Q) and a morphism of algebras Cl(Q) → A.

This universal property is expressed in Mathlib as CliffordAlgebra.lift. We can witness some of its properties as follows:

open CliffordAlgebra

variable (A : Type*) [Ring A] [Algebra R A]
  (f : M →ₗ[R] A)
  (hf : ∀ m, f m * f m = algebraMap _ _ (Q m))

-- The spelling `hf` above is convenient below and is
-- trivially equivalent to the more familiar spelling.
example (m : M) :
    f m * f m = algebraMap _ _ (Q m) ↔
    (f m) ^ 2 = Q m • 1 := byR:Type u_1M:Type u_2inst✝⁴:CommRing Rinst✝³:AddCommGroup Minst✝²:Module R MQ:QuadraticForm R MA:Type u_3inst✝¹:Ring Ainst✝:Algebra R Af:M →ₗ[R] Ahf:∀ (m : M), f m * f m = (algebraMap R A) (Q m)m:M⊢ f m * f m = (algebraMap R A) (Q m) ↔ f m ^ 2 = Q m • 1
  simp [sq, Algebra.smul_def, mul_one]All goals completed! 🐙

-- The induced map, as a morphism of algebras:
(lift Q) ⟨f, hf⟩ : CliffordAlgebra Q →ₐ[R] A#check lift Q ⟨f, hf⟩

-- This is a factorisation of our original map:
example : lift Q ⟨f, hf⟩ ∘ ι Q = f := byR:Type u_1M:Type u_2inst✝⁴:CommRing Rinst✝³:AddCommGroup Minst✝²:Module R MQ:QuadraticForm R MA:Type u_3inst✝¹:Ring Ainst✝:Algebra R Af:M →ₗ[R] Ahf:∀ (m : M), f m * f m = (algebraMap R A) (Q m)⊢ ⇑((lift Q) ⟨f, hf⟩) ∘ ⇑(ι Q) = ⇑f
  extR:Type u_1M:Type u_2inst✝⁴:CommRing Rinst✝³:AddCommGroup Minst✝²:Module R MQ:QuadraticForm R MA:Type u_3inst✝¹:Ring Ainst✝:Algebra R Af:M →ₗ[R] Ahf:∀ (m : M), f m * f m = (algebraMap R A) (Q m)x✝:M⊢ (⇑((lift Q) ⟨f, hf⟩) ∘ ⇑(ι Q)) x✝ = f x✝; simpAll goals completed! 🐙