lim : (J ⥤ C) ⥤ C is lax monoidal when C is a monoidal category.

When C is a monoidal category, the limit functor lim : (J ⥤ C) ⥤ C is lax monoidal, i.e. there are morphisms

• (𝟙_ C) → limit (𝟙_ (J ⥤ C))
• limit F ⊗ limit G ⟶ limit (F ⊗ G) satisfying the laws of a lax monoidal functor.

TODO

Now that we have oplax monoidal functors, assemble Limits.colim into an oplax monoidal functor.

instance CategoryTheory.Limits.instLaxMonoidalFunctorLim {J : Type w} [SmallCategory J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] [MonoidalCategory C] : lim.LaxMonoidal

Equations

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

@[simp]

theorem CategoryTheory.Limits.lim_ε_π {J : Type w} [SmallCategory J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] [MonoidalCategory C] (j : J) : CategoryStruct.comp (Functor.LaxMonoidal.ε lim) (limit.π (𝟙_ (Functor J C)) j) = CategoryStruct.id (𝟙_ C)

@[simp]

theorem CategoryTheory.Limits.lim_ε_π_assoc {J : Type w} [SmallCategory J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] [MonoidalCategory C] (j : J) {Z : C} (h : (𝟙_ (Functor J C)).obj j ⟶ Z) : CategoryStruct.comp (Functor.LaxMonoidal.ε lim) (CategoryStruct.comp (limit.π (𝟙_ (Functor J C)) j) h) = h

@[simp]

theorem CategoryTheory.Limits.lim_μ_π {J : Type w} [SmallCategory J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] [MonoidalCategory C] (F G : Functor J C) (j : J) : CategoryStruct.comp (Functor.LaxMonoidal.μ lim F G) (limit.π (MonoidalCategoryStruct.tensorObj F G) j) = MonoidalCategoryStruct.tensorHom (limit.π F j) (limit.π G j)

@[simp]

theorem CategoryTheory.Limits.lim_μ_π_assoc {J : Type w} [SmallCategory J] {C : Type u} [Category.{v, u} C] [HasLimitsOfShape J C] [MonoidalCategory C] (F G : Functor J C) (j : J) {Z : C} (h : (MonoidalCategoryStruct.tensorObj F G).obj j ⟶ Z) : CategoryStruct.comp (Functor.LaxMonoidal.μ lim F G) (CategoryStruct.comp (limit.π (MonoidalCategoryStruct.tensorObj F G) j) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (limit.π F j) (limit.π G j)) h