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 CategoryTheory.Mon.limit {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : Mon C

We construct the limit object of a functor F : J ⥤ Mon C given a limit cone c of F ⋙ forget C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Mon.limit_X {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (limit F c hc).X = c.pt

@[simp]

theorem CategoryTheory.Mon.limit_mon_one {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : MonObj.one = hc.lift { pt := MonoidalCategoryStruct.tensorUnit C, π := { app := fun (X : J) => MonObj.one, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Mon.limit_mon_mul {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : MonObj.mul = hc.lift { pt := MonoidalCategoryStruct.tensorObj c.1 c.1, π := { app := fun (X : J) => CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (c.π.app X) (c.π.app X)) MonObj.mul, naturality := ⋯ } }

def CategoryTheory.Mon.limitCone {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : Limits.Cone F

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

Equations

• CategoryTheory.Mon.limitCone F c hc = { pt := CategoryTheory.Mon.limit F c hc, π := { app := fun (j : J) => CategoryTheory.Mon.Hom.mk' (c.π.app j) ⋯ ⋯, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Mon.limitCone_π_app_hom {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) (j : J) : ((limitCone F c hc).π.app j).hom = c.π.app j

@[simp]

theorem CategoryTheory.Mon.limitCone_pt {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (limitCone F c hc).pt = limit F c hc

def CategoryTheory.Mon.forgetMapConeLimitConeIso {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (forget C).mapCone (limitCone F c hc) ≅ 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

• CategoryTheory.Mon.forgetMapConeLimitConeIso F c hc = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl ((CategoryTheory.Mon.forget C).mapCone (CategoryTheory.Mon.limitCone F c hc)).pt) ⋯

@[simp]

theorem CategoryTheory.Mon.forgetMapConeLimitConeIso_hom_hom {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (forgetMapConeLimitConeIso F c hc).hom.hom = CategoryStruct.id c.pt

@[simp]

theorem CategoryTheory.Mon.forgetMapConeLimitConeIso_inv_hom {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : (forgetMapConeLimitConeIso F c hc).inv.hom = CategoryStruct.id c.pt

def CategoryTheory.Mon.limitConeIsLimit {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : Limits.IsLimit (limitCone F c hc)

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 CategoryTheory.Mon.limitConeIsLimit_lift_hom {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) (s : Limits.Cone F) : ((limitConeIsLimit F c hc).lift s).hom = hc.lift ((forget C).mapCone s)

def CategoryTheory.Mon.limitConeLiftsToLimit {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) (c : Limits.Cone (F.comp (forget C))) (hc : Limits.IsLimit c) : LiftsToLimit F (forget C) c hc

A helper definition to show that the forgetful functor forget C : Mon C ⥤ C creates limits: given a limit cone c of F ⋙ forget C, we can lift it to a limit cone of F.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CategoryTheory.Mon.instCreatesLimitForget {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (F : Functor J (Mon C)) : CreatesLimit F (forget C)

Equations

• CategoryTheory.Mon.instCreatesLimitForget F = CategoryTheory.createsLimitOfReflectsIso (CategoryTheory.Mon.limitConeLiftsToLimit F)

@[implicit_reducible]

instance CategoryTheory.Mon.instCreatesLimitsOfShapeForget {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : CreatesLimitsOfShape J (forget C)

Equations

• CategoryTheory.Mon.instCreatesLimitsOfShapeForget = { CreatesLimit := fun {K : CategoryTheory.Functor J (CategoryTheory.Mon C)} => inferInstance }

@[implicit_reducible]

instance CategoryTheory.Mon.instCreatesLimitsOfSizeForget {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : CreatesLimitsOfSize.{w, u_1, v, v, max u v, u} (forget C)

Equations

• CategoryTheory.Mon.instCreatesLimitsOfSizeForget = { CreatesLimitsOfShape := fun {J : Type ?u.22} [CategoryTheory.Category.{?u.23, ?u.22} J] => inferInstance }

@[implicit_reducible]

instance CategoryTheory.Mon.instCreatesLimitsForget {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : CreatesLimits (forget C)

Equations

• CategoryTheory.Mon.instCreatesLimitsForget = { CreatesLimitsOfShape := fun {J : Type ?u.28} [CategoryTheory.Category.{?u.28, ?u.28} J] => inferInstance }

instance CategoryTheory.Mon.instHasLimitsOfShape {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasLimitsOfShape J C] : Limits.HasLimitsOfShape J (Mon C)

instance CategoryTheory.Mon.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape {J : Type w} [Category.{v_1, w} J] {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasLimitsOfShape J C] : Limits.PreservesLimitsOfShape J (forget C)