Limits of monoid objects. #
If C has limits, so does Mon_ C, and the forgetful functor preserves these limits.
(This could potentially replace many individual constructions for concrete categories,
in particular MonCat, SemiRingCat, RingCat, and AlgebraCat R.)
@[simp]
theorem
Mon_.limit_one
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
(Mon_.limit F).one = CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F (Mon_.forget C))
((CategoryTheory.Limits.Cones.postcompose
(CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Inverse.obj F).one).obj
{ pt := CategoryTheory.MonoidalCategory.tensorUnit',
π :=
CategoryTheory.NatTrans.mk fun j =>
CategoryTheory.CategoryStruct.id CategoryTheory.MonoidalCategory.tensorUnit' })
@[simp]
theorem
Mon_.limit_mul
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
(Mon_.limit F).mul = CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F (Mon_.forget C))
((CategoryTheory.Limits.Cones.postcompose
(CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Inverse.obj F).mul).obj
{
pt :=
CategoryTheory.MonoidalCategory.tensorObj
(CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F (Mon_.forget C)))
(CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F (Mon_.forget C))),
π :=
CategoryTheory.NatTrans.mk fun j =>
CategoryTheory.MonoidalCategory.tensorHom
(CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F (Mon_.forget C)) j)
(CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F (Mon_.forget C)) j) })
@[simp]
theorem
Mon_.limit_X
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
def
Mon_.limit
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
Mon_ C
We construct the (candidate) limit of a functor F : J ⥤ Mon_ C
by interpreting it as a functor Mon_ (J ⥤ C),
and noting that taking limits is a lax monoidal functor,
and hence sends monoid objects to monoid objects.
Instances For
@[simp]
theorem
Mon_.limitCone_pt
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
(Mon_.limitCone F).pt = Mon_.limit F
@[simp]
theorem
Mon_.limitCone_π_app_hom
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
(j : J)
:
((Mon_.limitCone F).π.app j).hom = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F (Mon_.forget C)) j
def
Mon_.limitCone
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
Implementation of Mon_.hasLimits: a limiting cone over a functor F : J ⥤ Mon_ C.
Instances For
def
Mon_.forgetMapConeLimitConeIso
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
(Mon_.forget C).mapCone (Mon_.limitCone F) ≅ CategoryTheory.Limits.limit.cone (CategoryTheory.Functor.comp F (Mon_.forget C))
The image of the proposed limit cone for F : J ⥤ Mon_ C under the forgetful functor
forget C : Mon_ C ⥤ C is isomorphic to the limit cone of F ⋙ forget C.
Instances For
@[simp]
theorem
Mon_.limitConeIsLimit_lift_hom
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
(s : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.IsLimit.lift (Mon_.limitConeIsLimit F) s).hom = CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F (Mon_.forget C)) ((Mon_.forget C).mapCone s)
def
Mon_.limitConeIsLimit
{J : Type v}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
Implementation of Mon_.hasLimits:
the proposed cone over a functor F : J ⥤ Mon_ C is a limit cone.
Instances For
instance
Mon_.hasLimits
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimits C]
[CategoryTheory.MonoidalCategory C]
: