# mathlibdocumentation

category_theory.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

• lim_lax.ε : (𝟙_ C) → limit (𝟙_ (J ⥤ C))
• lim_lax.μ : limit F ⊗ limit G ⟶ limit (F ⊗ G) satisfying the laws of a lax monoidal functor.
@[protected, instance]
noncomputable def category_theory.limits.limit_functorial {J : Type v} {C : Type u}  :
Equations
@[simp]
theorem category_theory.limits.limit_functorial_map {J : Type v} {C : Type u} {F G : J C} (α : F G) :
category_theory.map (λ (F : J C), α =
@[simp]
theorem category_theory.limits.limit_lax_monoidal_μ {J : Type v} {C : Type u} (F G : J C) :
category_theory.lax_monoidal.μ (λ (F : J C), F G = {X := , π := {app := λ (j : J), , naturality' := _}}
@[protected, instance]
noncomputable def category_theory.limits.limit_lax_monoidal {J : Type v} {C : Type u}  :
Equations
@[simp]
theorem category_theory.limits.limit_lax_monoidal_ε {J : Type v} {C : Type u}  :
category_theory.lax_monoidal.ε (λ (F : J C), = {X := 𝟙_ C _inst_4, π := {app := λ (j : J), 𝟙 (𝟙_ C)).obj j), naturality' := _}}
noncomputable def category_theory.limits.lim_lax {J : Type v} {C : Type u}  :

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

Equations
@[simp]
theorem category_theory.limits.lim_lax_obj {J : Type v} {C : Type u} (F : J C) :
theorem category_theory.limits.lim_lax_obj' {J : Type v} {C : Type u} (F : J C) :
@[simp]
theorem category_theory.limits.lim_lax_map {J : Type v} {C : Type u} {F G : J C} (α : F G) :
@[simp]
theorem category_theory.limits.lim_lax_ε {J : Type v} {C : Type u}  :
category_theory.limits.lim_lax.ε = {X := 𝟙_ C _inst_4, π := {app := λ (j : J), 𝟙 (𝟙_ C)).obj j), naturality' := _}}
@[simp]
theorem category_theory.limits.lim_lax_μ {J : Type v} {C : Type u} (F G : J C) :
= {X := , π := {app := λ (j : J), , naturality' := _}}