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}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
:
CategoryTheory.Limits.lim.LaxMonoidal
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.lim_ε_π
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(j : J)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim)
(CategoryTheory.Limits.limit.π (𝟙_ (CategoryTheory.Functor J C)) j) = CategoryTheory.CategoryStruct.id (𝟙_ C)
@[simp]
theorem
CategoryTheory.Limits.lim_ε_π_assoc
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(j : J)
{Z : C}
(h : (𝟙_ (CategoryTheory.Functor J C)).obj j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (𝟙_ (CategoryTheory.Functor J C)) j) h) = h
@[simp]
theorem
CategoryTheory.Limits.lim_μ_π
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F G : CategoryTheory.Functor J C)
(j : J)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim F G)
(CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategory.tensorObj F G) j) = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.limit.π F j) (CategoryTheory.Limits.limit.π G j)
@[simp]
theorem
CategoryTheory.Limits.lim_μ_π_assoc
{J : Type w}
[CategoryTheory.SmallCategory J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.MonoidalCategory C]
(F G : CategoryTheory.Functor J C)
(j : J)
{Z : C}
(h : (CategoryTheory.MonoidalCategory.tensorObj F G).obj j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim F G)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategory.tensorObj F G) j) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.limit.π F j) (CategoryTheory.Limits.limit.π G j))
h