Limits in Grp C

We show that Grp C has limits.

instance CategoryTheory.instPreservesLimitsOfShapeMonFunctorOppositeMonCatShrinkYonedaMon {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] : Limits.PreservesLimitsOfShape J shrinkYonedaMon.{max w v, v, u_1}

noncomputable def CategoryTheory.Grp.limitAux {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] (F : Functor J (Grp C)) : Grp C

An auxillary construction in order to prove that Grp.forget₂Mon creates limits.

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.instCreatesLimitsOfShapeGrpMonForget₂Mon {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] : CreatesLimitsOfShape J (Grp.forget₂Mon C)

Equations

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

@[implicit_reducible]

noncomputable instance CategoryTheory.instCreatesLimitsOfShapeGrpForget {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] : CreatesLimitsOfShape J (Grp.forget C)

Equations

• CategoryTheory.instCreatesLimitsOfShapeGrpForget = inferInstanceAs (CategoryTheory.CreatesLimitsOfShape J ((CategoryTheory.Grp.forget₂Mon C).comp (CategoryTheory.Mon.forget C)))

instance CategoryTheory.instHasLimitsOfShapeGrp {C : Type u_1} [Category.{v, u_1} C] [CartesianMonoidalCategory C] {J : Type w} [Category.{u_2, w} J] [Limits.HasLimitsOfShape J C] : Limits.HasLimitsOfShape J (Grp C)