Documentation

Mathlib.CategoryTheory.Functor.Trifunctor

Trifunctors obtained by composition of bifunctors #

Given two bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂ and G : C₁₂ ⥤ C₃ ⥤ C₄, we define the trifunctor bifunctorComp₁₂ F₁₂ G : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which sends three objects X₁ : C₁, X₂ : C₂ and X₃ : C₃ to G.obj ((F₁₂.obj X₁).obj X₂)).obj X₃.

Similarly, given two bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄ and G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃, we define the trifunctor bifunctorComp₂₃ F G₂₃ : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ which sends three objects X₁ : C₁, X₂ : C₂ and X₃ : C₃ to (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃).

@[simp]
theorem CategoryTheory.bifunctorComp₁₂Obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) (X₁ : C₁) {X₂ : C₂} {Y₂ : C₂} (φ : X₂ Y₂) (X₃ : C₃) :
((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).map φ).app X₃ = (G.map ((F₁₂.obj X₁).map φ)).app X₃
@[simp]
theorem CategoryTheory.bifunctorComp₁₂Obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).obj X₃ = (G.obj ((F₁₂.obj X₁).obj X₂)).obj X₃
@[simp]
theorem CategoryTheory.bifunctorComp₁₂Obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) (X₁ : C₁) (X₂ : C₂) :
∀ {x x_1 : C₃} (φ : x x_1), ((CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂).map φ = (G.obj ((F₁₂.obj X₁).obj X₂)).map φ

Auxiliary definition for bifunctorComp₁₂.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.bifunctorComp₁₂_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {X₁ : C₁} {Y₁ : C₁} (φ : X₁ Y₁) (X₂ : C₂) (X₃ : C₃) :
    (((CategoryTheory.bifunctorComp₁₂ F₁₂ G).map φ).app X₂).app X₃ = (G.map ((F₁₂.map φ).app X₂)).app X₃

    Given two bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂ and G : C₁₂ ⥤ C₃ ⥤ C₄, this is the trifunctor C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ obtained by composition.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.bifunctorComp₂₃Obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X₁ : C₁) (X₂ : C₂) :
      ∀ {x x_1 : C₃} (φ : x x_1), ((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).map φ = (F.obj X₁).map ((G₂₃.obj X₂).map φ)
      @[simp]
      theorem CategoryTheory.bifunctorComp₂₃Obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X₁ : C₁) {X₂ : C₂} {Y₂ : C₂} (φ : X₂ Y₂) (X₃ : C₃) :
      ((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).map φ).app X₃ = (F.obj X₁).map ((G₂₃.map φ).app X₃)
      @[simp]
      theorem CategoryTheory.bifunctorComp₂₃Obj_obj_obj {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
      ((CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁).obj X₂).obj X₃ = (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃)

      Auxiliary definition for bifunctorComp₂₃.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.bifunctorComp₂₃_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {X₁ : C₁} {Y₁ : C₁} (φ : X₁ Y₁) (X₂ : C₂) (X₃ : C₃) :
        (((CategoryTheory.bifunctorComp₂₃ F G₂₃).map φ).app X₂).app X₃ = (F.map φ).app ((G₂₃.obj X₂).obj X₃)

        Given two bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄ and G₂₃ : C₂ ⥤ C₃ ⥤ C₄, this is the trifunctor C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄ obtained by composition.

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