Documentation

Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Tensor product of colimits #

In this file, we apply the PreservesColimit₂ API to the bifunctor curriedTensor C on a monoidal category C.

Given cocones c₁ and c₂ for functors F₁ : J₁ ⥤ C and F₂ : J₂ ⥤ C, we define a cocone c₁.tensor₂ c₂ for the functor J₁ × J₂ ⥤ C obtained using the tensor product on C, and we obtain that it is a colimit cocone if both c₁ and c₂ are, and PreservesColimit₂ F₁ F₂ (curriedTensor C) holds.

We also introduce a definition Cocone.tensor which takes as an input two cocones c₁ and c₂ for two functors F₁ : J ⥤ C and F₂ : J ⥤ C and produces a cocone for F₁ ⊗ F₂ : J ⥤ C with point c₁.pt ⊗ c₂.pt and we show that it is a colimit cocone when PreservesColimit₂ F₁ F₂ (curriedTensor C) holds and J is sifted.

source
@[reducible, inline]
abbrev CategoryTheory.Limits.Cocone.tensor₂ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {J₁ : Type u_3} {J₂ : Type u_4} [Category.{v_3, u_3} J₁] [Category.{v_4, u_4} J₂] {F₁ : Functor J₁ C} {F₂ : Functor J₂ C} (c₁ : Cocone F₁) (c₂ : Cocone F₂) :
Cocone (MonoidalCategory.externalProduct F₁ F₂)

The external tensor product of two cocones.

Equations
Instances For
    source
    noncomputable def CategoryTheory.Limits.IsColimit.tensor₂ {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {J₁ : Type u_3} {J₂ : Type u_4} [Category.{v_3, u_3} J₁] [Category.{v_4, u_4} J₂] {F₁ : Functor J₁ C} {F₂ : Functor J₂ C} {c₁ : Cocone F₁} {c₂ : Cocone F₂} [PreservesColimit₂ F₁ F₂ (MonoidalCategory.curriedTensor C)] (hc₁ : IsColimit c₁) (hc₂ : IsColimit c₂) :
    IsColimit (c₁.tensor₂ c₂)

    The external tensor product of colimit cocones for functors F₁ : J₁ ⥤ C and F₂ : J₂ ⥤ C is a colimit cocone when PreservesColimit₂ F₁ F₂ (curriedTensor C) holds.

    Equations
    Instances For
      source
      def CategoryTheory.Limits.Cocone.tensor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] {F₁ F₂ : Functor J C} (c₁ : Cocone F₁) (c₂ : Cocone F₂) :
      Cocone (MonoidalCategoryStruct.tensorObj F₁ F₂)

      The tensor product of two cocones.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Limits.Cocone.tensor_ι_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] {F₁ F₂ : Functor J C} (c₁ : Cocone F₁) (c₂ : Cocone F₂) (j : J) :
        (c₁.tensor c₂).ι.app j = MonoidalCategoryStruct.tensorHom (c₁.ι.app j) (c₂.ι.app j)
        source
        @[simp]
        theorem CategoryTheory.Limits.Cocone.tensor_pt {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] {F₁ F₂ : Functor J C} (c₁ : Cocone F₁) (c₂ : Cocone F₂) :
        (c₁.tensor c₂).pt = MonoidalCategoryStruct.tensorObj c₁.pt c₂.pt
        source
        noncomputable def CategoryTheory.Limits.IsColimit.tensor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {J : Type u_2} [Category.{v_2, u_2} J] {F₁ F₂ : Functor J C} {c₁ : Cocone F₁} {c₂ : Cocone F₂} [PreservesColimit₂ F₁ F₂ (MonoidalCategory.curriedTensor C)] [IsSifted J] (hc₁ : IsColimit c₁) (hc₂ : IsColimit c₂) :
        IsColimit (c₁.tensor c₂)

        The tensor product of colimit cocones for functors F₁ : J ⥤ C and F₂ : J ⥤ C is a colimit cocone when PreservesColimit₂ F₁ F₂ (curriedTensor C) holds and J is sifted.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For