Limits of monoid objects. #
If C has limits (of a given shape), 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.)
def
Mon_.limit
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J 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.
Equations
- Mon_.limit F = CategoryTheory.Limits.lim.mapMon.obj ((CategoryTheory.Monoidal.monFunctorCategoryEquivalence J C).inverse.obj F)
@[simp]
theorem
Mon_.limit_X
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
(Mon_.limit F).X = CategoryTheory.Limits.limit (F.comp (Mon_.forget C))
@[simp]
theorem
Mon_.limit_mul
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
(Mon_.limit F).mul = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim (F.comp (Mon_.forget C)) (F.comp (Mon_.forget C)))
(CategoryTheory.Limits.limMap (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).mul)
@[simp]
theorem
Mon_.limit_one
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
(Mon_.limit F).one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim)
(CategoryTheory.Limits.limMap (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).one)
def
Mon_.limitCone
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
Implementation of Mon_.hasLimits: a limiting cone over a functor F : J ⥤ Mon_ C.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Mon_.limitCone_pt
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J 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 w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
(j : J)
:
((Mon_.limitCone F).π.app j).hom = CategoryTheory.Limits.limit.π (F.comp (Mon_.forget C)) j
def
Mon_.forgetMapConeLimitConeIso
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
(Mon_.forget C).mapCone (Mon_.limitCone F) ≅ CategoryTheory.Limits.limit.cone (F.comp (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.
Equations
- Mon_.forgetMapConeLimitConeIso F = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl ((Mon_.forget C).mapCone (Mon_.limitCone F)).pt) ⋯
def
Mon_.limitConeIsLimit
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
:
Implementation of Mon_.hasLimitsOfShape:
the proposed cone over a functor F : J ⥤ Mon_ C is a limit cone.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Mon_.limitConeIsLimit_lift_hom
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.Functor J (Mon_ C))
(s : CategoryTheory.Limits.Cone F)
:
((Mon_.limitConeIsLimit F).lift s).hom = CategoryTheory.Limits.limit.lift (F.comp (Mon_.forget C)) ((Mon_.forget C).mapCone s)
instance
Mon_.hasLimitsOfShape
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
:
Equations
- ⋯ = ⋯
instance
Mon_.forget_freservesLimitsOfShape
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
:
Equations
- ⋯ = ⋯