coyonedaObjIsoForget — Mathlib

English

The coyoneda corepresentation for AddMonCat is isomorphic to the forgetful functor; i.e., coyoneda.obj(op(of ULift Nat)) ≅ forget AddMonCat.

Русский

Койнoеда–ядро представления AddMonCat изоморфно забывающему функтору; то есть Coyoneda.obj(op(of ULift Nat)) ≅ forget AddMonCat.

LaTeX

$$$\mathrm{coyoneda.obj}(\mathrm{op}(\mathrm{of}(\mathrm{ULift}.(\mathrm{Nat})))) \cong \mathrm{forget AddMonCat}$$$

Lean4

/-- The forgetful functor `AddMonCat.{u} ⥤ Type u` is corepresentable. -/
def coyonedaObjIsoForget : coyoneda.obj (op (of (ULift.{u} ℕ))) ≅ forget AddMonCat.{u} :=
  NatIso.ofComponents fun M ↦ (ConcreteCategory.homEquiv.trans (uliftMultiplesHom M.carrier).symm).toIso

Похожие утверждения