lim : (J ⥤ C) ⥤ C is lax monoidal when C is a monoidal category. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C] :
category_theory.functorial (λ (F : J ⥤ C), category_theory.limits.limit F)
Equations
@[simp]
theorem
category_theory.limits.limit_functorial_map
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
{F G : J ⥤ C}
(α : F ⟶ G) :
category_theory.map (λ (F : J ⥤ C), category_theory.limits.limit F) α = category_theory.limits.lim.map α
@[simp]
theorem
category_theory.limits.limit_lax_monoidal_μ
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F G : J ⥤ C) :
category_theory.lax_monoidal.μ (λ (F : J ⥤ C), category_theory.limits.limit F) F G = category_theory.limits.limit.lift (F ⊗ G) {X := category_theory.limits.limit F ⊗ category_theory.limits.limit G, π := {app := λ (j : J), category_theory.limits.limit.π F j ⊗ category_theory.limits.limit.π G j, naturality' := _}}
@[protected, instance]
noncomputable
def
category_theory.limits.limit_lax_monoidal
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C] :
category_theory.lax_monoidal (λ (F : J ⥤ C), category_theory.limits.limit F)
Equations
- category_theory.limits.limit_lax_monoidal = {ε := category_theory.limits.limit.lift ((category_theory.functor.const J).obj (𝟙_ C)) {X := 𝟙_ C _inst_4, π := {app := λ (j : J), 𝟙 (((category_theory.functor.const J).obj (𝟙_ C)).obj j), naturality' := _}}, μ := λ (F G : J ⥤ C), category_theory.limits.limit.lift (F ⊗ G) {X := category_theory.limits.limit F ⊗ category_theory.limits.limit G, π := {app := λ (j : J), category_theory.limits.limit.π F j ⊗ category_theory.limits.limit.π G j, naturality' := _}}, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}
@[simp]
theorem
category_theory.limits.limit_lax_monoidal_ε
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C] :
category_theory.lax_monoidal.ε (λ (F : J ⥤ C), category_theory.limits.limit F) = category_theory.limits.limit.lift ((category_theory.functor.const J).obj (𝟙_ C)) {X := 𝟙_ C _inst_4, π := {app := λ (j : J), 𝟙 (((category_theory.functor.const J).obj (𝟙_ C)).obj j), naturality' := _}}
noncomputable
def
category_theory.limits.lim_lax
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C] :
The limit functor F ↦ limit F bundled as a lax monoidal functor.
Equations
@[simp]
theorem
category_theory.limits.lim_lax_obj
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ C) :
theorem
category_theory.limits.lim_lax_obj'
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F : J ⥤ C) :
@[simp]
theorem
category_theory.limits.lim_lax_map
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
{F G : J ⥤ C}
(α : F ⟶ G) :
@[simp]
theorem
category_theory.limits.lim_lax_ε
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C] :
category_theory.limits.lim_lax.ε = category_theory.limits.limit.lift ((category_theory.functor.const J).obj (𝟙_ C)) {X := 𝟙_ C _inst_4, π := {app := λ (j : J), 𝟙 (((category_theory.functor.const J).obj (𝟙_ C)).obj j), naturality' := _}}
@[simp]
theorem
category_theory.limits.lim_lax_μ
{J : Type v}
[category_theory.small_category J]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits C]
[category_theory.monoidal_category C]
(F G : J ⥤ C) :
category_theory.limits.lim_lax.μ F G = category_theory.limits.limit.lift (F ⊗ G) {X := category_theory.limits.limit F ⊗ category_theory.limits.limit G, π := {app := λ (j : J), category_theory.limits.limit.π F j ⊗ category_theory.limits.limit.π G j, naturality' := _}}