English
There is a free-forgetful adjunction between CommRingCat and its forgetful functor to the underlying type category.
Русский
Существует пара взаимно противоположных адъюнкций между CommRingCat и забывающим функтором к базовой категории типов.
LaTeX
$$$\text{adj} : \text{free} \dashv \text{forget}$$$
Lean4
/-- The free-forgetful adjunction for commutative rings. -/
def adj : free ⊣ forget CommRingCat.{u} :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun _ _ ↦
{ toFun := fun f ↦ homEquiv f.hom
invFun := fun f ↦ ofHom <| homEquiv.symm f
left_inv := fun f ↦ congrArg ofHom (homEquiv.left_inv f.hom)
right_inv := fun f ↦ homEquiv.right_inv f }
homEquiv_naturality_left_symm := fun {_ _ Y} f g =>
hom_ext <| RingHom.ext fun x ↦ eval₂_cast_comp f (Int.castRingHom Y) g x }
