Currying of functors in three variables

We study the equivalence of categories currying₃ : (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ≌ C₁ × C₂ × C₃ ⥤ E.

def CategoryTheory.currying₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : Functor C₁ (Functor C₂ (Functor C₃ E)) ≌ Functor (C₁ × C₂ × C₃) E

The equivalence of categories (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ≌ C₁ × C₂ × C₃ ⥤ E given by the curryfication of functors in three variables.

Equations

• CategoryTheory.currying₃ = CategoryTheory.currying.trans (CategoryTheory.currying.trans (CategoryTheory.prod.associativity C₁ C₂ C₃).congrLeft)

@[reducible, inline]

abbrev CategoryTheory.uncurry₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : Functor (Functor C₁ (Functor C₂ (Functor C₃ E))) (Functor (C₁ × C₂ × C₃) E)

Uncurrying a functor in three variables.

Equations

• CategoryTheory.uncurry₃ = CategoryTheory.currying₃.functor

@[reducible, inline]

abbrev CategoryTheory.curry₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : Functor (Functor (C₁ × C₂ × C₃) E) (Functor C₁ (Functor C₂ (Functor C₃ E)))

Currying a functor in three variables.

Equations

• CategoryTheory.curry₃ = CategoryTheory.currying₃.inverse

def CategoryTheory.fullyFaithfulUncurry₃ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] : uncurry₃.FullyFaithful

Uncurrying functors in three variables gives a fully faithful functor.

Equations

• CategoryTheory.fullyFaithfulUncurry₃ = CategoryTheory.currying₃.fullyFaithfulFunctor

@[simp]

theorem CategoryTheory.curry₃_obj_map_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor (C₁ × C₂ × C₃) E) {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) (X₂ : C₂) (X₃ : C₃) : (((curry₃.obj F).map f).app X₂).app X₃ = F.map (f, CategoryStruct.id X₂, CategoryStruct.id X₃)

@[simp]

theorem CategoryTheory.curry₃_obj_obj_map_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor (C₁ × C₂ × C₃) E) (X₁ : C₁) {X₂ Y₂ : C₂} (f : X₂ ⟶ Y₂) (X₃ : C₃) : (((curry₃.obj F).obj X₁).map f).app X₃ = F.map (CategoryStruct.id X₁, f, CategoryStruct.id X₃)

@[simp]

theorem CategoryTheory.curry₃_obj_obj_obj_map {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] (F : Functor (C₁ × C₂ × C₃) E) (X₁ : C₁) (X₂ : C₂) {X₃ Y₃ : C₃} (f : X₃ ⟶ Y₃) : (((curry₃.obj F).obj X₁).obj X₂).map f = F.map (CategoryStruct.id X₁, CategoryStruct.id X₂, f)

@[simp]

theorem CategoryTheory.curry₃_map_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_9} E] {F G : Functor (C₁ × C₂ × C₃) E} (f : F ⟶ G) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((curry₃.map f).app X₁).app X₂).app X₃ = f.app (X₁, X₂, X₃)

@[simp]

theorem CategoryTheory.currying₃_unitIso_hom_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_13, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_11, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((currying₃.unitIso.hom.app F).app X₁).app X₂).app X₃ = CategoryStruct.id (((((Functor.id (Functor C₁ (Functor C₂ (Functor C₃ E)))).obj F).obj X₁).obj X₂).obj X₃)

@[simp]

theorem CategoryTheory.currying₃_unitIso_inv_app_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_13, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_11, u_9} E] (F : Functor C₁ (Functor C₂ (Functor C₃ E))) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((currying₃.unitIso.inv.app F).app X₁).app X₂).app X₃ = CategoryStruct.id (((((currying₃.functor.comp currying₃.inverse).obj F).obj X₁).obj X₂).obj X₃)

def CategoryTheory.curry₃ObjProdComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_6} D₁] [Category.{u_14, u_7} D₂] [Category.{u_15, u_8} D₃] [Category.{u_16, u_9} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (G : Functor (D₁ × D₂ × D₃) E) : curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G) ≅ F₁.comp ((curry₃.obj G).comp (((whiskeringLeft₂ E).obj F₂).obj F₃))

Given functors F₁ : C₁ ⥤ D₁, F₂ : C₂ ⥤ D₂, F₃ : C₃ ⥤ D₃ and G : D₁ × D₂ × D₃ ⥤ E, this is the isomorphism between curry₃.obj (F₁.prod (F₂.prod F₃) ⋙ G) : C₁ ⥤ C₂ ⥤ C₃ ⥤ E and F₁ ⋙ curry₃.obj G ⋙ ((whiskeringLeft₂ E).obj F₂).obj F₃.

Equations

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

@[simp]

theorem CategoryTheory.curry₃ObjProdComp_inv_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_6} D₁] [Category.{u_14, u_7} D₂] [Category.{u_15, u_8} D₃] [Category.{u_16, u_9} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (G : Functor (D₁ × D₂ × D₃) E) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((curry₃ObjProdComp F₁ F₂ F₃ G).inv.app X).app X✝).app X✝ = CategoryStruct.id ((((curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G)).obj X).obj X✝).obj X✝)

@[simp]

theorem CategoryTheory.curry₃ObjProdComp_hom_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {D₁ : Type u_6} {D₂ : Type u_7} {D₃ : Type u_8} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_6} D₁] [Category.{u_14, u_7} D₂] [Category.{u_15, u_8} D₃] [Category.{u_16, u_9} E] (F₁ : Functor C₁ D₁) (F₂ : Functor C₂ D₂) (F₃ : Functor C₃ D₃) (G : Functor (D₁ × D₂ × D₃) E) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((curry₃ObjProdComp F₁ F₂ F₃ G).hom.app X).app X✝).app X✝ = CategoryStruct.id ((((curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G)).obj X).obj X✝).obj X✝)

def CategoryTheory.bifunctorComp₁₂Iso {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_3} C₁₂] [Category.{u_14, u_9} E] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ E)) : bifunctorComp₁₂ F₁₂ G ≅ curry.obj ((uncurry.obj F₁₂).comp G)

bifunctorComp₁₂ can be described in terms of the curryfication of functors.

Equations

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

@[simp]

theorem CategoryTheory.bifunctorComp₁₂Iso_inv_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_3} C₁₂] [Category.{u_14, u_9} E] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ E)) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((bifunctorComp₁₂Iso F₁₂ G).inv.app X).app X✝).app X✝ = CategoryStruct.id ((G.obj ((F₁₂.obj X).obj X✝)).obj X✝)

@[simp]

theorem CategoryTheory.bifunctorComp₁₂Iso_hom_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_4} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_3} C₁₂] [Category.{u_14, u_9} E] (F₁₂ : Functor C₁ (Functor C₂ C₁₂)) (G : Functor C₁₂ (Functor C₃ E)) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((bifunctorComp₁₂Iso F₁₂ G).hom.app X).app X✝).app X✝ = CategoryStruct.id ((G.obj ((F₁₂.obj X).obj X✝)).obj X✝)

def CategoryTheory.bifunctorComp₂₃Iso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {C₂₃ : Type u_5} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_5} C₂₃] [Category.{u_14, u_9} E] (F : Functor C₁ (Functor C₂₃ E)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) : bifunctorComp₂₃ F G₂₃ ≅ curry.obj (curry.obj ((prod.associator C₁ C₂ C₃).comp (uncurry.obj ((uncurry.obj G₂₃).comp F.flip).flip)))

bifunctorComp₂₃ can be described in terms of the curryfication of functors.

Equations

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

@[simp]

theorem CategoryTheory.bifunctorComp₂₃Iso_hom_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {C₂₃ : Type u_5} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_5} C₂₃] [Category.{u_14, u_9} E] (F : Functor C₁ (Functor C₂₃ E)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((bifunctorComp₂₃Iso F G₂₃).hom.app X).app X✝).app X✝ = CategoryStruct.id ((F.obj X).obj ((G₂₃.obj X✝).obj X✝))

@[simp]

theorem CategoryTheory.bifunctorComp₂₃Iso_inv_app_app_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {C₂₃ : Type u_5} {E : Type u_9} [Category.{u_10, u_1} C₁] [Category.{u_11, u_2} C₂] [Category.{u_12, u_4} C₃] [Category.{u_13, u_5} C₂₃] [Category.{u_14, u_9} E] (F : Functor C₁ (Functor C₂₃ E)) (G₂₃ : Functor C₂ (Functor C₃ C₂₃)) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((bifunctorComp₂₃Iso F G₂₃).inv.app X).app X✝).app X✝ = CategoryStruct.id ((F.obj X).obj ((G₂₃.obj X✝).obj X✝))