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

• limLax.ε : (𝟙_ C) → limit (𝟙_ (J ⥤ C))
• limLax.μ : 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.limitFunctorial {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] : CategoryTheory.Functorial fun (F : CategoryTheory.Functor J C) => CategoryTheory.Limits.limit F

Equations

• CategoryTheory.Limits.limitFunctorial = { map' := fun {X Y : CategoryTheory.Functor J C} => CategoryTheory.Limits.lim.map, map_id' := ⋯, map_comp' := ⋯ }

@[simp]

theorem CategoryTheory.Limits.limitFunctorial_map {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ⟶ G) : CategoryTheory.map (fun (F : CategoryTheory.Functor J C) => CategoryTheory.Limits.limit F) α = CategoryTheory.Limits.lim.map α

@[simp]

theorem CategoryTheory.Limits.limitLaxMonoidal_μ {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 C) (G : CategoryTheory.Functor J C) : CategoryTheory.LaxMonoidal.μ F G = CategoryTheory.Limits.limit.lift (CategoryTheory.MonoidalCategory.tensorObj F G) { pt := CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.Limits.limit F) (CategoryTheory.Limits.limit G), π := { app := fun (j : J) => CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.limit.π F j) (CategoryTheory.Limits.limit.π G j), naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Limits.limitLaxMonoidal_ε {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.LaxMonoidal.ε = CategoryTheory.Limits.limit.lift ((CategoryTheory.Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun (j : J) => CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj (𝟙_ C)).obj j), naturality := ⋯ } }

instance CategoryTheory.Limits.limitLaxMonoidal {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.LaxMonoidal fun (F : CategoryTheory.Functor J C) => CategoryTheory.Limits.limit F

Equations

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

def CategoryTheory.Limits.limLax {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Functor J C) C

The limit functor F ↦ limit F bundled as a lax monoidal functor.

Equations

• CategoryTheory.Limits.limLax = CategoryTheory.LaxMonoidalFunctor.of fun (F : CategoryTheory.Functor J C) => CategoryTheory.Limits.limit F

@[simp]

theorem CategoryTheory.Limits.limLax_obj {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 C) : CategoryTheory.Limits.limLax.obj F = CategoryTheory.Limits.limit F

theorem CategoryTheory.Limits.limLax_obj' {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 C) : CategoryTheory.Limits.limLax.obj F = CategoryTheory.Limits.lim.obj F

@[simp]

theorem CategoryTheory.Limits.limLax_map {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 C} {G : CategoryTheory.Functor J C} (α : F ⟶ G) : CategoryTheory.Limits.limLax.map α = CategoryTheory.Limits.lim.map α

@[simp]

theorem CategoryTheory.Limits.limLax_ε {J : Type w} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Limits.limLax.ε = CategoryTheory.Limits.limit.lift ((CategoryTheory.Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun (j : J) => CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj (𝟙_ C)).obj j), naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Limits.limLax_μ {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 C) (G : CategoryTheory.Functor J C) : CategoryTheory.Limits.limLax.μ F G = CategoryTheory.Limits.limit.lift (CategoryTheory.MonoidalCategory.tensorObj F G) { pt := CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.Limits.limit F) (CategoryTheory.Limits.limit G), π := { app := fun (j : J) => CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.limit.π F j) (CategoryTheory.Limits.limit.π G j), naturality := ⋯ } }