English
There is an adjunction between the free R-algebra functor and the forgetful functor from AlgCat R to RingCat; i.e., Free_R ⊣ Forget.
Русский
Существует смежность между свободной R-алгеброй и забывающим функтором: Free_R ⊣ Forget.
LaTeX
$$$\\mathrm{Free}_R \\dashv \\mathrm{Forget}_{\\mathrm{AlgCat}(R)\\to \\mathrm{RingCat}}$$$
Lean4
/-- The free/forget adjunction for `R`-algebras. -/
def adj : free.{u} R ⊣ forget (AlgCat.{u} R) :=
Adjunction.mkOfHomEquiv
{
homEquiv := fun _ _ =>
{ toFun := fun f ↦ (FreeAlgebra.lift _).symm f.hom
invFun := fun f ↦ ofHom <| (FreeAlgebra.lift _) f
left_inv := fun f ↦ by aesop
right_inv := fun f ↦ by simp [forget_obj] } }
