coyonedaObjIsoForget — Mathlib

English

For any f: j ⟶ j', the map F.map f followed by coconeMorphism equals the coconeMorphism at j; i.e., naturality of the cocone morphisms with respect to F.map f.

Русский

Для любого f: j ⟶ j' отображение F.map f после коконного морфизма равно коконному морфизму на j; то есть натуральность коконных морфизмов относительно F.map f.

LaTeX

$$$F.map f \; \circ \mathrm{coconeMorphism}_{F}(j') = \mathrm{coconeMorphism}_{F}(j)$$$

Lean4

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

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