# 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.
Equations
• CategoryTheory.Limits.limitFunctorial = { map' := fun {X Y : } => CategoryTheory.Limits.lim.map, map_id' := , map_comp' := }
@[simp]
theorem CategoryTheory.Limits.limitFunctorial_map {J : Type v} {C : Type u} {F : } {G : } (α : F G) :
CategoryTheory.map (fun (F : ) => ) α = CategoryTheory.Limits.lim.map α
@[simp]
theorem CategoryTheory.Limits.limitLaxMonoidal_μ {J : Type v} {C : Type u} (F : ) (G : ) :
= CategoryTheory.Limits.limit.lift { pt := , π := { app := fun (j : J) => , naturality := } }
@[simp]
theorem CategoryTheory.Limits.limitLaxMonoidal_ε {J : Type v} {C : Type u} :
CategoryTheory.LaxMonoidal.ε = CategoryTheory.Limits.limit.lift (.obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun (j : J) => CategoryTheory.CategoryStruct.id ((.obj (𝟙_ C)).obj j), naturality := } }
Equations
• One or more equations did not get rendered due to their size.

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

Equations
• CategoryTheory.Limits.limLax =
Instances For
@[simp]
theorem CategoryTheory.Limits.limLax_obj {J : Type v} {C : Type u} (F : ) :
CategoryTheory.Limits.limLax.obj F =
theorem CategoryTheory.Limits.limLax_obj' {J : Type v} {C : Type u} (F : ) :
CategoryTheory.Limits.limLax.obj F = CategoryTheory.Limits.lim.obj F
@[simp]
theorem CategoryTheory.Limits.limLax_map {J : Type v} {C : Type u} {F : } {G : } (α : F G) :
CategoryTheory.Limits.limLax.map α = CategoryTheory.Limits.lim.map α
@[simp]
theorem CategoryTheory.Limits.limLax_ε {J : Type v} {C : Type u} :
CategoryTheory.Limits.limLax = CategoryTheory.Limits.limit.lift (.obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun (j : J) => CategoryTheory.CategoryStruct.id ((.obj (𝟙_ C)).obj j), naturality := } }
@[simp]
theorem CategoryTheory.Limits.limLax_μ {J : Type v} {C : Type u} (F : ) (G : ) :
CategoryTheory.Limits.limLax F G = CategoryTheory.Limits.limit.lift { pt := , π := { app := fun (j : J) => , naturality := } }