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 AlgCat 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_mon_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_Class.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim) (CategoryTheory.Limits.limMap Mon_Class.one)

@[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)) : (limit F).X = CategoryTheory.Limits.limit (F.comp (forget C))

@[simp]

theorem Mon_.limit_mon_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_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim (F.comp (forget C)) (F.comp (forget C))) (CategoryTheory.Limits.limMap Mon_Class.mul)

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)) : CategoryTheory.Limits.Cone F

Implementation of Mon_.hasLimits: a limiting cone over a functor F : J ⥤ Mon_ C.

Equations

• Mon_.limitCone F = { pt := Mon_.limit F, π := { app := fun (j : J) => Mon_.Hom.mk' (CategoryTheory.Limits.limit.π (F.comp (Mon_.forget C)) j) ⋯ ⋯, naturality := ⋯ } }

@[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) : ((limitCone F).π.app j).hom = CategoryTheory.Limits.limit.π (F.comp (forget C)) j

@[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)) : (limitCone F).pt = limit F

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)) : (forget C).mapCone (limitCone F) ≅ CategoryTheory.Limits.limit.cone (F.comp (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)) : CategoryTheory.Limits.IsLimit (limitCone F)

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) : ((limitConeIsLimit F).lift s).hom = CategoryTheory.Limits.limit.lift (F.comp (forget C)) ((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] : CategoryTheory.Limits.HasLimitsOfShape J (Mon_ C)

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] : CategoryTheory.Limits.PreservesLimitsOfShape J (forget C)