Miscellany about preservations of (co)limits in monoidal categories #
This file records some PreservesColimits instance on tensors products on monoidal categories.
instance
CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_left
{C : Type u_1}
[Category.{u_3, u_1} C]
[MonoidalCategory C]
{J : Type u_2}
[Category.{u_4, u_2} J]
(F : Functor J C)
[BraidedCategory C]
(c : C)
[Limits.PreservesColimit F (tensorLeft c)]
:
When C is braided and tensorLeft c preserves a colimit, then so does tensorRight k.
theorem
CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_right
{C : Type u_1}
[Category.{u_3, u_1} C]
[MonoidalCategory C]
{J : Type u_2}
[Category.{u_4, u_2} J]
(F : Functor J C)
[BraidedCategory C]
(c : C)
[Limits.PreservesColimit F (tensorRight c)]
:
When C is braided and tensorRight c preserves a colimit, then so does tensorLeft k.
We are not making this an instance to avoid an instance loop with
preservesColimit_of_braided_and_preservesColimit_tensor_left.
theorem
CategoryTheory.MonoidalCategory.Limits.preservesCoLimit_curriedTensor
{C : Type u_1}
[Category.{u_4, u_1} C]
[MonoidalCategory C]
{J : Type u_2}
[Category.{u_3, u_2} J]
(F : Functor J C)
[h : ∀ (c : C), Limits.PreservesColimit F (tensorRight c)]
:
instance
CategoryTheory.MonoidalCategory.Limits.preservesLimit_of_braided_and_preservesLimit_tensor_left
{C : Type u_1}
[Category.{u_3, u_1} C]
[MonoidalCategory C]
{J : Type u_2}
[Category.{u_4, u_2} J]
(F : Functor J C)
[BraidedCategory C]
(c : C)
[Limits.PreservesLimit F (tensorLeft c)]
:
When C is braided and tensorLeft c preserves a limit, then so does tensorRight k.
theorem
CategoryTheory.MonoidalCategory.Limits.preservesLimit_of_braided_and_preservesLimit_tensor_right
{C : Type u_1}
[Category.{u_3, u_1} C]
[MonoidalCategory C]
{J : Type u_2}
[Category.{u_4, u_2} J]
(F : Functor J C)
[BraidedCategory C]
(c : C)
[Limits.PreservesLimit F (tensorRight c)]
:
When C is braided and tensorRight c preserves a limit, then so does tensorLeft k.
We are not making this an instance to avoid an instance loop with
preservesLimit_of_braided_and_preservesLimit_tensor_left.
theorem
CategoryTheory.MonoidalCategory.Limits.preservesLimit_curriedTensor
{C : Type u_1}
[Category.{u_4, u_1} C]
[MonoidalCategory C]
{J : Type u_2}
[Category.{u_3, u_2} J]
(F : Functor J C)
[h : ∀ (c : C), Limits.PreservesLimit F (tensorRight c)]
: