coyonedaObjIsoForget — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{coyoneda.obj}(\mathrm{op}(\mathrm{of}(\mathrm{ULift}(\mathbb{N})))) \cong \mathrm{forget AddCommMonCat}$$$

Lean4

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

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