lim : (J ⥤ C) ⥤ C is lax monoidal when C is a monoidal category. #
When C is a monoidal category, the limit functor lim : (J ⥤ C) ⥤ C is lax monoidal,
i.e. there are morphisms
(𝟙_ C) → limit (𝟙_ (J ⥤ C))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.instLaxMonoidalFunctorLim
{J : Type w}
[SmallCategory J]
{C : Type u}
[Category.{v, u} C]
[HasLimitsOfShape J C]
[MonoidalCategory C]
:
lim.LaxMonoidal
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.lim_ε_π
{J : Type w}
[SmallCategory J]
{C : Type u}
[Category.{v, u} C]
[HasLimitsOfShape J C]
[MonoidalCategory C]
(j : J)
:
CategoryStruct.comp (Functor.LaxMonoidal.ε lim) (limit.π (𝟙_ (Functor J C)) j) = CategoryStruct.id (𝟙_ C)
@[simp]
theorem
CategoryTheory.Limits.lim_ε_π_assoc
{J : Type w}
[SmallCategory J]
{C : Type u}
[Category.{v, u} C]
[HasLimitsOfShape J C]
[MonoidalCategory C]
(j : J)
{Z : C}
(h : (𝟙_ (Functor J C)).obj j ⟶ Z)
:
CategoryStruct.comp (Functor.LaxMonoidal.ε lim) (CategoryStruct.comp (limit.π (𝟙_ (Functor J C)) j) h) = h
@[simp]
theorem
CategoryTheory.Limits.lim_μ_π
{J : Type w}
[SmallCategory J]
{C : Type u}
[Category.{v, u} C]
[HasLimitsOfShape J C]
[MonoidalCategory C]
(F G : Functor J C)
(j : J)
:
CategoryStruct.comp (Functor.LaxMonoidal.μ lim F G) (limit.π (MonoidalCategoryStruct.tensorObj F G) j) = MonoidalCategoryStruct.tensorHom (limit.π F j) (limit.π G j)
@[simp]
theorem
CategoryTheory.Limits.lim_μ_π_assoc
{J : Type w}
[SmallCategory J]
{C : Type u}
[Category.{v, u} C]
[HasLimitsOfShape J C]
[MonoidalCategory C]
(F G : Functor J C)
(j : J)
{Z : C}
(h : (MonoidalCategoryStruct.tensorObj F G).obj j ⟶ Z)
:
CategoryStruct.comp (Functor.LaxMonoidal.μ lim F G)
(CategoryStruct.comp (limit.π (MonoidalCategoryStruct.tensorObj F G) j) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (limit.π F j) (limit.π G j)) h