Miscellany about preservation of (co)limits in monoidal categories

This file records some PreservesColimits instances on tensor products in monoidal categories.

instance CategoryTheory.MonoidalCategory.Limits.preservesColimit_of_braided_and_preservesColimit_tensor_left {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] (F : Functor J C) [BraidedCategory C] (c : C) [Limits.PreservesColimit F (tensorLeft c)] : Limits.PreservesColimit F (tensorRight 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.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] (F : Functor J C) [BraidedCategory C] (c : C) [Limits.PreservesColimit F (tensorRight c)] : Limits.PreservesColimit F (tensorLeft 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.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] (F : Functor J C) [h : ∀ (c : C), Limits.PreservesColimit F (tensorRight c)] : Limits.PreservesColimit F (curriedTensor C)

@[deprecated CategoryTheory.MonoidalCategory.Limits.preservesColimit_curriedTensor (since := "2026-09-17")]

theorem CategoryTheory.MonoidalCategory.Limits.preservesCoLimit_curriedTensor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] (F : Functor J C) [h : ∀ (c : C), Limits.PreservesColimit F (tensorRight c)] : Limits.PreservesColimit F (curriedTensor C)

Alias of CategoryTheory.MonoidalCategory.Limits.preservesColimit_curriedTensor.

instance CategoryTheory.MonoidalCategory.Limits.preservesLimit_of_braided_and_preservesLimit_tensor_left {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] (F : Functor J C) [BraidedCategory C] (c : C) [Limits.PreservesLimit F (tensorLeft c)] : Limits.PreservesLimit F (tensorRight 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.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] (F : Functor J C) [BraidedCategory C] (c : C) [Limits.PreservesLimit F (tensorRight c)] : Limits.PreservesLimit F (tensorLeft 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.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] (F : Functor J C) [h : ∀ (c : C), Limits.PreservesLimit F (tensorRight c)] : Limits.PreservesLimit F (curriedTensor C)