English
The Coyoneda embedding valued in CommGrpCat composed with the forgetful functor is the usual Coyoneda embedding.
Русский
Кояонеда-встраивание, взятое в значение для CommGrpCat и композиция с функтором забывания, совпадает с обычным Coyoneda.
LaTeX
$$$\mathrm{coyoneda}_{\CommGrpCat} \circ U \cong \mathrm{coyoneda}_{\mathbf{Type}}$$$
Lean4
/-- The `CommGrpCat`-valued coyoneda embedding composed with the forgetful functor is the usual
coyoneda embedding. -/
@[to_additive (attr := simps!) /--
The `AddCommGrpCat`-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 }
