English
Let CommGrpCat be the category of commutative groups and let U: CommGrpCat → Type be the forgetful functor to sets. There exists a representing object for U in the opposite category, namely the ULift of the multiplicative integers, such that coyoneda at that object is naturally isomorphic to U. In other words, U is corepresentable by the object ULift(Multiplicative ℤ).
Русский
Пусть CommGrpCat — категория коммутативных групп, и возьмём забывающий функтор U: CommGrpCat → Type (множество). Существует представляемый объект в противоположной категории, который корепрезентирует U; конкретно ULift(Multiplicative ℤ) служит корепрезентантом, так что Coyoneda opd(ULift(Multiplicative ℤ)) изоморфно forgetting.
LaTeX
$$$ \\mathrm{coyoneda}\\big(\\mathrm{op}(\\mathrm{of}(\\mathrm{ULift}(\\mathrm{Multiplicative}\\, \\mathbb{Z})))\\big) \\cong \\mathrm{forget}\\, \\mathrm{CommGrpCat}^{\,u} $$$
Lean4
/-- The forget functor `CommGrpCat.{u} ⥤ Type u` is corepresentable. -/
def coyonedaObjIsoForget : coyoneda.obj (op (of (ULift.{u} (Multiplicative ℤ)))) ≅ forget CommGrpCat.{u} :=
NatIso.ofComponents fun M ↦ (ConcreteCategory.homEquiv.trans (uliftZPowersHom M.carrier).symm).toIso
