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.limLax.mapMon.obj ((CategoryTheory.Monoidal.monFunctorCategoryEquivalence J C).inverse.obj F)
Instances For
@[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.Limits.limit.lift (F.comp (Mon_.forget C))
((CategoryTheory.Limits.Cones.postcompose
(CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).mul).obj
{
pt :=
CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.Limits.limit (F.comp (Mon_.forget C)))
(CategoryTheory.Limits.limit (F.comp (Mon_.forget C))),
π :=
{
app := fun (j : J) =>
CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.limit.π (F.comp (Mon_.forget C)) j)
(CategoryTheory.Limits.limit.π (F.comp (Mon_.forget C)) j),
naturality := ⋯ } })
@[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.Limits.limit.lift (F.comp (Mon_.forget C))
((CategoryTheory.Limits.Cones.postcompose
(CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).one).obj
{ pt := 𝟙_ C, π := { app := fun (x : J) => CategoryTheory.CategoryStruct.id (𝟙_ C), naturality := ⋯ } })
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.
Instances For
@[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) ⋯
Instances For
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_.hasLimits:
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.
Instances For
@[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_.forgetPreservesLimitsOfShape
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
:
Equations
- One or more equations did not get rendered due to their size.