English
There is a natural isomorphism yonedaGrpObj X ≅ F whenever F is Representable by X (in the GrpCat context).
Русский
Существует естественный изоморфизм yonedaGrpObj X ≅ F, когда F представим как X (в контексте GrpCat).
LaTeX
$$$\yonedaGrpObj X \cong F$ (if F is RepresentableBy X)$$
Lean4
/-- If `X` represents a presheaf of groups `F`, then `Hom(-, X)` is isomorphic to `F` as
a presheaf of groups. -/
@[simps! hom inv]
def yonedaGrpObjIsoOfRepresentableBy (F : Cᵒᵖ ⥤ GrpCat.{v}) (α : (F ⋙ forget _).RepresentableBy X) :
letI := GrpObj.ofRepresentableBy X F α
yonedaGrpObj X ≅ F :=
letI := GrpObj.ofRepresentableBy X F α
NatIso.ofComponents
(fun Y ↦
MulEquiv.toGrpIso
{ toEquiv := α.homEquiv
map_mul' := ((yonedaMonObjIsoOfRepresentableBy X (F ⋙ forget₂ GrpCat MonCat) α).hom.app Y).hom.map_mul })
fun φ ↦ GrpCat.hom_ext <| MonoidHom.ext <| α.homEquiv_comp φ.unop
