Yoneda embedding of CommMon_ C #
theorem
IsCommMonObj.ofRepresentableBy
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : C)
(F : CategoryTheory.Functor Cᵒᵖ CommMonCat)
(α : (F.comp (CategoryTheory.forget CommMonCat)).RepresentableBy X)
:
If X represents a presheaf of commutative monoids, then X is a commutative monoid object.
@[deprecated IsCommMonObj.ofRepresentableBy (since := "2025-09-14")]
theorem
IsCommMon.ofRepresentableBy
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : C)
(F : CategoryTheory.Functor Cᵒᵖ CommMonCat)
(α : (F.comp (CategoryTheory.forget CommMonCat)).RepresentableBy X)
:
Alias of IsCommMonObj.ofRepresentableBy.
If X represents a presheaf of commutative monoids, then X is a commutative monoid object.