English
If M is a monoid object, then the presheaf Hom(-, M) is representable by M; there is a canonical isomorphism between yonedaMonObj M and the presheaf F that represents M.
Русский
Если M является моноидным объектом, то предобъект Hom(-, M) представлен M; существует каноническое изоморфное отображение между yonedaMonObj M и представляемой F.
LaTeX
$$$\\yonedaMonObj M \\cong F$ ( representable by M )$$
Lean4
/-- If `X` represents a presheaf of monoids `F`, then `Hom(-, X)` is isomorphic to `F` as
a presheaf of monoids. -/
@[simps!]
def yonedaMonObjIsoOfRepresentableBy (F : Cᵒᵖ ⥤ MonCat.{v}) (α : (F ⋙ forget _).RepresentableBy X) :
letI := MonObj.ofRepresentableBy X F α
yonedaMonObj X ≅ F :=
letI := MonObj.ofRepresentableBy X F α
NatIso.ofComponents
(fun Y ↦
MulEquiv.toMonCatIso
{ toEquiv := α.homEquiv
map_mul' f₁
f₂ :=
by
change
α.homEquiv (lift f₁ f₂ ≫ α.homEquiv.symm (α.homEquiv (fst X X) * α.homEquiv (snd X X))) =
α.homEquiv f₁ * α.homEquiv f₂
simp only [α.homEquiv_comp, Equiv.apply_symm_apply, Functor.comp_map, ConcreteCategory.forget_map_eq_coe,
map_mul]
simp only [← Functor.comp_map, ← ConcreteCategory.forget_map_eq_coe, ← α.homEquiv_comp]
simp })
(fun φ ↦ MonCat.hom_ext (MonoidHom.ext (α.homEquiv_comp φ.unop)))
