English
Two algebra homomorphisms g and lift Q ⟨f, cond⟩ agree on ι_Q if and only if g equals the lift of f; i.e., the lift is the universal extension with a unique property.
Русский
Два алгебра-гомоморфизма g и подъем через Q совпадают на ι_Q тогда и только тогда, когда g равняется подъему от f; т. е. подъем является универсальным продолжением.
LaTeX
$$$g.toLinearMap \\circ ι_Q = f \\;\\land\\; g = \\mathrm{lift}\\ Q ⟨f, cond⟩ \\quad\\Longrightarrow\\quad g = \\mathrm{lift}\\ Q ⟨f, cond⟩$$$
Lean4
@[simp]
theorem lift_unique (f : M →ₗ[R] A) (cond : ∀ m : M, f m * f m = algebraMap _ _ (Q m)) (g : CliffordAlgebra Q →ₐ[R] A) :
g.toLinearMap.comp (ι Q) = f ↔ g = lift Q ⟨f, cond⟩ :=
by
convert (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).symm_apply_eq
rw [lift_symm_apply, Subtype.mk_eq_mk]
