English
The lift map provides a universal correspondence between linear maps M → A and algebra morphisms TensorAlgebra R M →ₐ[R] A.
Русский
Пусть есть линейное отображение M → A; его можно единственным образом поднять до алгебрового гомоморфа из TensorAlgebra R M в A.
LaTeX
$$lift : (M →ₗ[R] A) ≃ (TensorAlgebra R M →ₐ[R] A)$$
Lean4
/-- Given a linear map `f : M → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
of `f` to a morphism of `R`-algebras `TensorAlgebra R M → A`.
-/
@[simps symm_apply]
def lift {A : Type*} [Semiring A] [Algebra R A] : (M →ₗ[R] A) ≃ (TensorAlgebra R M →ₐ[R] A) :=
{ toFun :=
RingQuot.liftAlgHom R ∘ fun f =>
⟨FreeAlgebra.lift R (⇑f), fun x y (h : Rel R M x y) => by
induction h <;>
simp only [Algebra.smul_def, FreeAlgebra.lift_ι_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, map_mul,
AlgHom.commutes, map_add]⟩
invFun := fun F => F.toLinearMap.comp (ι R)
left_inv := fun f => by
rw [ι]
ext1 x
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply f x)
right_inv := fun F =>
RingQuot.ringQuot_ext' _ _ _ <|
FreeAlgebra.hom_ext <|
funext fun x => by
rw [ι]
exact (RingQuot.liftAlgHom_mkAlgHom_apply _ _ _ _).trans (FreeAlgebra.lift_ι_apply _ _) }
