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