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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_9} E] : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)) ≌ CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_9} E] : CategoryTheory.Functor (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_9} E] : CategoryTheory.Functor (CategoryTheory.Functor (C₁ × C₂ × C₃) E) (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_9} E] : CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_9} E] (F : CategoryTheory.Functor (C₁ × C₂ × C₃) E) {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁) (X₂ : C₂) (X₃ : C₃) : (((CategoryTheory.curry₃.obj F).map f).app X₂).app X₃ = F.map (f, CategoryTheory.CategoryStruct.id X₂, CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_9} E] (F : CategoryTheory.Functor (C₁ × C₂ × C₃) E) (X₁ : C₁) {X₂ Y₂ : C₂} (f : X₂ ⟶ Y₂) (X₃ : C₃) : (((CategoryTheory.curry₃.obj F).obj X₁).map f).app X₃ = F.map (CategoryTheory.CategoryStruct.id X₁, f, CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_9} E] (F : CategoryTheory.Functor (C₁ × C₂ × C₃) E) (X₁ : C₁) (X₂ : C₂) {X₃ Y₃ : C₃} (f : X₃ ⟶ Y₃) : (((CategoryTheory.curry₃.obj F).obj X₁).obj X₂).map f = F.map (CategoryTheory.CategoryStruct.id X₁, CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_9} E] {F G : CategoryTheory.Functor (C₁ × C₂ × C₃) E} (f : F ⟶ G) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_11, u_9} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((CategoryTheory.currying₃.unitIso.hom.app F).app X₁).app X₂).app X₃ = CategoryTheory.CategoryStruct.id (((((CategoryTheory.Functor.id (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_13, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_11, u_9} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) : (((CategoryTheory.currying₃.unitIso.inv.app F).app X₁).app X₂).app X₃ = CategoryTheory.CategoryStruct.id (((((CategoryTheory.currying₃.functor.comp CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_6} D₁] [CategoryTheory.Category.{u_14, u_7} D₂] [CategoryTheory.Category.{u_15, u_8} D₃] [CategoryTheory.Category.{u_16, u_9} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (G : CategoryTheory.Functor (D₁ × D₂ × D₃) E) : CategoryTheory.curry₃.obj ((F₁.prod (F₂.prod F₃)).comp G) ≅ F₁.comp ((CategoryTheory.curry₃.obj G).comp (((CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_6} D₁] [CategoryTheory.Category.{u_14, u_7} D₂] [CategoryTheory.Category.{u_15, u_8} D₃] [CategoryTheory.Category.{u_16, u_9} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (G : CategoryTheory.Functor (D₁ × D₂ × D₃) E) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((CategoryTheory.curry₃ObjProdComp F₁ F₂ F₃ G).inv.app X).app X✝).app X✝ = CategoryTheory.CategoryStruct.id ((((CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_6} D₁] [CategoryTheory.Category.{u_14, u_7} D₂] [CategoryTheory.Category.{u_15, u_8} D₃] [CategoryTheory.Category.{u_16, u_9} E] (F₁ : CategoryTheory.Functor C₁ D₁) (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃) (G : CategoryTheory.Functor (D₁ × D₂ × D₃) E) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((CategoryTheory.curry₃ObjProdComp F₁ F₂ F₃ G).hom.app X).app X✝).app X✝ = CategoryTheory.CategoryStruct.id ((((CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_3} C₁₂] [CategoryTheory.Category.{u_14, u_9} E] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ E)) : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.curry.obj ((CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_3} C₁₂] [CategoryTheory.Category.{u_14, u_9} E] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ E)) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((CategoryTheory.bifunctorComp₁₂Iso F₁₂ G).inv.app X).app X✝).app X✝ = CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_3} C₁₂] [CategoryTheory.Category.{u_14, u_9} E] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ E)) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((CategoryTheory.bifunctorComp₁₂Iso F₁₂ G).hom.app X).app X✝).app X✝ = CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_5} C₂₃] [CategoryTheory.Category.{u_14, u_9} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ E)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) : CategoryTheory.bifunctorComp₂₃ F G₂₃ ≅ CategoryTheory.curry.obj (CategoryTheory.curry.obj ((CategoryTheory.prod.associator C₁ C₂ C₃).comp (CategoryTheory.uncurry.obj ((CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_5} C₂₃] [CategoryTheory.Category.{u_14, u_9} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ E)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((CategoryTheory.bifunctorComp₂₃Iso F G₂₃).hom.app X).app X✝).app X✝ = CategoryTheory.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} [CategoryTheory.Category.{u_10, u_1} C₁] [CategoryTheory.Category.{u_11, u_2} C₂] [CategoryTheory.Category.{u_12, u_4} C₃] [CategoryTheory.Category.{u_13, u_5} C₂₃] [CategoryTheory.Category.{u_14, u_9} E] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ E)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X : C₁) (X✝ : C₂) (X✝ : C₃) : (((CategoryTheory.bifunctorComp₂₃Iso F G₂₃).inv.app X).app X✝).app X✝ = CategoryTheory.CategoryStruct.id ((F.obj X).obj ((G₂₃.obj X✝).obj X✝))