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_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)) : MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim (F.comp (forget C)) (F.comp (forget C))) (CategoryTheory.Limits.limMap MonObj.mul)

@[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)) : MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim) (CategoryTheory.Limits.limMap MonObj.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))

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_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

@[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

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_preservesLimitsOfShape {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)