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

TODO #

Now that we have oplax monoidal functors, assemble Limits.colim into an oplax monoidal functor.

Equations
  • CategoryTheory.Limits.limitFunctorial = { map' := fun {X Y : CategoryTheory.Functor J C} => CategoryTheory.Limits.lim.map, map_id' := , map_comp' := }
@[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 := } }
@[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 := } }