English
There is a natural bijection between linear maps f: M → A that satisfy f(m)^2 = Q(m) (for all m) and R-algebra homomorphisms Clifford(Q) → A. The correspondence sends f to the unique lift to an algebra homomorphism and recovers f by restriction to ι_Q.
Русский
Существует естественная биекция между линейными отображениями f: M → A с условием f(m)^2 = Q(m) и R-алгебра-гомоморфизмами Clifford(Q) → A; отображение fℎ переходит в уникальный подъем к алгебра-гомоморфизму и восстанавливает f по ограничению к ι_Q.
LaTeX
$$$\\{ f : M \\to_ R A \\;|\\; ∀m, f(m)^2 = \\mathrm{algebraMap}_R(Q(m)) \\} \\cong Clifford(Q) \\to_ R A,$ with the forward map $f \\mapsto (\\mathrm{lift}\\ Q \\langle f, \\text{cond} \\rangle)$ and inverse $g \\mapsto g \\circ ι_Q$.$$
Lean4
/-- 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`.
-/
@[simps symm_apply]
def lift : { f : M →ₗ[R] A // ∀ m, f m * f m = algebraMap _ _ (Q m) } ≃ (CliffordAlgebra Q →ₐ[R] A)
where
toFun
f :=
RingQuot.liftAlgHom R
⟨TensorAlgebra.lift R (f : M →ₗ[R] A), fun x y (h : Rel Q x y) =>
by
induction h
rw [AlgHom.commutes, map_mul, TensorAlgebra.lift_ι_apply, f.prop]⟩
invFun
F := ⟨F.toLinearMap.comp (ι Q), fun m => by rw [LinearMap.comp_apply, AlgHom.toLinearMap_apply, comp_ι_sq_scalar]⟩
left_inv
f := by
ext x
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ x)
right_inv
F :=
RingQuot.ringQuot_ext' _ _ _ <|
TensorAlgebra.hom_ext <|
LinearMap.ext fun x ↦ (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (TensorAlgebra.lift_ι_apply _ _)
