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₃).
def
CategoryTheory.bifunctorComp₁₂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₁)
:
CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)
Auxiliary definition for bifunctorComp₁₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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 φ
def
CategoryTheory.bifunctorComp₁₂
{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₄))
:
CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))
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
{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₁)
:
(CategoryTheory.bifunctorComp₁₂ F₁₂ G).obj X₁ = CategoryTheory.bifunctorComp₁₂Obj F₁₂ G X₁
@[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₃
def
CategoryTheory.bifunctorComp₂₃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₁)
:
CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄)
Auxiliary definition for bifunctorComp₂₃.
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₃)
def
CategoryTheory.bifunctorComp₂₃
{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₂₃))
:
CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))
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₂₃_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₃)
@[simp]
theorem
CategoryTheory.bifunctorComp₂₃_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₁)
:
(CategoryTheory.bifunctorComp₂₃ F G₂₃).obj X₁ = CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁