theorem. Universal property [wieser2022formalizing] [ca-000C]

✍️source

CliffordAlgebra.ι_comp_liftCliffordAlgebra.lift_unique

L∃∀N

Given \(f : M \to _{l[R]} A\), which is Clifford, \(F = \operatorname {lift} f\) (denoted \(\bar {f}\) in some literatures), we have:

1. \(F \circ \iota = f\), i.e. the following diagram commutes:

   

2. \(\operatorname {lift}\) is unique, i.e. given \(G : \mathcal {C}\kern -2pt\ell (Q) \to _{a} A\), we have: \[ G \circ \iota = f \iff G = \operatorname {lift} f\]