Documentation

Mathlib.CategoryTheory.Monoidal.Limits

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

When C is a monoidal category, the functorial association F ↦ limit F is lax monoidal, i.e. there are morphisms

@[simp]
theorem CategoryTheory.Limits.limitLaxMonoidal_ε {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.MonoidalCategory C] :
CategoryTheory.LaxMonoidal.ε = CategoryTheory.Limits.limit.lift ((CategoryTheory.Functor.const J).obj CategoryTheory.MonoidalCategory.tensorUnit') { pt := CategoryTheory.MonoidalCategory.tensorUnit', π := CategoryTheory.NatTrans.mk fun j => CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj CategoryTheory.MonoidalCategory.tensorUnit').obj j) }
theorem CategoryTheory.Limits.limLax_obj' {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J C) :
CategoryTheory.Limits.limLax.toFunctor.obj F = CategoryTheory.Limits.lim.obj F
@[simp]
theorem CategoryTheory.Limits.limLax_map {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.MonoidalCategory C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F G) :
CategoryTheory.Limits.limLax.toFunctor.map α = CategoryTheory.Limits.lim.map α
@[simp]
theorem CategoryTheory.Limits.limLax_ε {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.MonoidalCategory C] :
CategoryTheory.Limits.limLax = CategoryTheory.Limits.limit.lift ((CategoryTheory.Functor.const J).obj CategoryTheory.MonoidalCategory.tensorUnit') { pt := CategoryTheory.MonoidalCategory.tensorUnit', π := CategoryTheory.NatTrans.mk fun j => CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj CategoryTheory.MonoidalCategory.tensorUnit').obj j) }