English
The coyoneda embedding for CommMonCat, after composing with the forgetful functor, agrees with the standard coyoneda embedding in the base category.
Русский
Кояонеда-встраивание для CommMonCat после композиции с забывающим функтором совпадает с обычнымCoyoneda-встраиванием в базовой категории.
LaTeX
$$$\text{coyonedaForget} : \mathrm{coyoneda} \circ \mathrm{forget} \cong \mathrm{coyoneda}$$$
Lean4
/-- The `CommMonCat`-valued coyoneda embedding composed with the forgetful functor is the usual
coyoneda embedding. -/
@[to_additive (attr := simps!) /--
The `AddCommMonCat`-valued coyoneda embedding composed with the forgetful functor is the usual
coyoneda embedding. -/
]
def coyonedaForget : coyoneda ⋙ (Functor.whiskeringRight _ _ _).obj (forget _) ≅ CategoryTheory.coyoneda :=
NatIso.ofComponents fun X ↦ NatIso.ofComponents fun Y ↦ { hom f := ofHom f, inv f := f.hom }
