# Curry and uncurry, as functors. #

We define curry : ((C × D) ⥤ E) ⥤ (C ⥤ (D ⥤ E)) and uncurry : (C ⥤ (D ⥤ E)) ⥤ ((C × D) ⥤ E), and verify that they provide an equivalence of categories currying : (C ⥤ (D ⥤ E)) ≌ ((C × D) ⥤ E).

@[simp]
theorem CategoryTheory.uncurry_obj_map {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) {X : C × D} {Y : C × D} (f : X Y) :
(CategoryTheory.uncurry.obj F).map f = CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
@[simp]
theorem CategoryTheory.uncurry_map_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] :
∀ {X Y : } (T : X Y) (X_1 : C × D), (CategoryTheory.uncurry.map T).app X_1 = (T.app X_1.1).app X_1.2
@[simp]
theorem CategoryTheory.uncurry_obj_obj {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) (X : C × D) :
(CategoryTheory.uncurry.obj F).obj X = (F.obj X.1).obj X.2
def CategoryTheory.uncurry {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] :

The uncurrying functor, taking a functor C ⥤ (D ⥤ E) and producing a functor (C × D) ⥤ E.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.curryObj {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : CategoryTheory.Functor (C × D) E) :

The object level part of the currying functor. (See curry for the functorial version.)

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.curry_obj_obj_map {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : CategoryTheory.Functor (C × D) E) (X : C) :
∀ {X_1 Y : D} (g : X_1 Y), ((CategoryTheory.curry.obj F).obj X).map g = F.map
@[simp]
theorem CategoryTheory.curry_obj_map_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : CategoryTheory.Functor (C × D) E) :
∀ {X Y : C} (f : X Y) (Y_1 : D), ((CategoryTheory.curry.obj F).map f).app Y_1 = F.map (f, )
@[simp]
theorem CategoryTheory.curry_obj_obj_obj {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D) :
((CategoryTheory.curry.obj F).obj X).obj Y = F.obj (X, Y)
@[simp]
theorem CategoryTheory.curry_map_app_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] :
∀ {X Y : CategoryTheory.Functor (C × D) E} (T : X Y) (X_1 : C) (Y_1 : D), ((CategoryTheory.curry.map T).app X_1).app Y_1 = T.app (X_1, Y_1)
def CategoryTheory.curry {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] :

The currying functor, taking a functor (C × D) ⥤ E and producing a functor C ⥤ (D ⥤ E).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.currying_inverse_obj_obj_obj {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D) :
((CategoryTheory.currying.inverse.obj F).obj X).obj Y = F.obj (X, Y)
@[simp]
theorem CategoryTheory.currying_inverse_map_app_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] :
∀ {X Y : CategoryTheory.Functor (C × D) E} (T : X Y) (X_1 : C) (Y_1 : D), ((CategoryTheory.currying.inverse.map T).app X_1).app Y_1 = T.app (X_1, Y_1)
@[simp]
theorem CategoryTheory.currying_functor_obj_map {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) {X : C × D} {Y : C × D} (f : X Y) :
(CategoryTheory.currying.functor.obj F).map f = CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
@[simp]
theorem CategoryTheory.currying_unitIso_hom_app_app_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (X : ) (X : C) (X : D) :
((CategoryTheory.currying.unitIso.hom.app X✝¹).app X✝).app X = CategoryTheory.CategoryStruct.id ((X✝¹.obj X✝).obj X)
@[simp]
theorem CategoryTheory.currying_functor_obj_obj {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) (X : C × D) :
(CategoryTheory.currying.functor.obj F).obj X = (F.obj X.1).obj X.2
@[simp]
theorem CategoryTheory.currying_inverse_obj_obj_map {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : CategoryTheory.Functor (C × D) E) (X : C) :
∀ {X_1 Y : D} (g : X_1 Y), ((CategoryTheory.currying.inverse.obj F).obj X).map g = F.map
@[simp]
theorem CategoryTheory.currying_unitIso_inv_app_app_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (X : ) (X : C) (X : D) :
((CategoryTheory.currying.unitIso.inv.app X✝¹).app X✝).app X = CategoryTheory.CategoryStruct.id ((X✝¹.obj X✝).obj X)
@[simp]
theorem CategoryTheory.currying_inverse_obj_map_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : CategoryTheory.Functor (C × D) E) :
∀ {X Y : C} (f : X Y) (Y_1 : D), ((CategoryTheory.currying.inverse.obj F).map f).app Y_1 = F.map (f, )
@[simp]
theorem CategoryTheory.currying_functor_map_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] :
∀ {X Y : } (T : X Y) (X_1 : C × D), (CategoryTheory.currying.functor.map T).app X_1 = (T.app X_1.1).app X_1.2
@[simp]
theorem CategoryTheory.currying_counitIso_hom_app_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (X : CategoryTheory.Functor (C × D) E) (X : C × D) :
(CategoryTheory.currying.counitIso.hom.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.obj (X.1, X.2))
@[simp]
theorem CategoryTheory.currying_counitIso_inv_app_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (X : CategoryTheory.Functor (C × D) E) (X : C × D) :
(CategoryTheory.currying.counitIso.inv.app X✝).app X = CategoryTheory.CategoryStruct.id (X✝.obj (X.1, X.2))
def CategoryTheory.currying {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] :

The equivalence of functor categories given by currying/uncurrying.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.flipIsoCurrySwapUncurry_inv_app_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) (X : D) (X : C) :
(.app X✝).app X = CategoryTheory.CategoryStruct.id ((F.obj X).obj X✝)
@[simp]
theorem CategoryTheory.flipIsoCurrySwapUncurry_hom_app_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) (X : D) (X : C) :
(.app X✝).app X = CategoryTheory.CategoryStruct.id ((F.obj X).obj X✝)
def CategoryTheory.flipIsoCurrySwapUncurry {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) :
F.flip CategoryTheory.curry.obj (.comp (CategoryTheory.uncurry.obj F))

F.flip is isomorphic to uncurrying F, swapping the variables, and currying.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.uncurryObjFlip_hom_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) (X : D × C) :
.hom.app X = CategoryTheory.CategoryStruct.id ((F.obj X.2).obj X.1)
@[simp]
theorem CategoryTheory.uncurryObjFlip_inv_app {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) (X : D × C) :
.inv.app X = CategoryTheory.CategoryStruct.id ((F.obj X.2).obj X.1)
def CategoryTheory.uncurryObjFlip {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] (F : ) :
CategoryTheory.uncurry.obj F.flip .comp (CategoryTheory.uncurry.obj F)

The uncurrying of F.flip is isomorphic to swapping the factors followed by the uncurrying of F.

Equations
Instances For
@[simp]
theorem CategoryTheory.whiskeringRight₂_map_app_app_app (B : Type u₁) [] (C : Type u₂) [] (D : Type u₃) [] (E : Type u₄) [] :
∀ {X Y : } (f : X Y) (X_1 : ) (Y_1 : ) (c : B), (((.map f).app X_1).app Y_1).app c = (f.app (X_1.obj c)).app (Y_1.obj c)
@[simp]
theorem CategoryTheory.whiskeringRight₂_obj_obj_obj_map (B : Type u₁) [] (C : Type u₂) [] (D : Type u₃) [] (E : Type u₄) [] (X : ) (X : ) (Y : ) :
∀ {X_1 Y_1 : B} (f : X_1 Y_1), (((.obj X✝).obj X).obj Y).map f = CategoryTheory.CategoryStruct.comp ((X✝.map (X.map f)).app (Y.obj X_1)) ((X✝.obj (X.obj Y_1)).map (Y.map f))
@[simp]
theorem CategoryTheory.whiskeringRight₂_obj_obj_obj_obj (B : Type u₁) [] (C : Type u₂) [] (D : Type u₃) [] (E : Type u₄) [] (X : ) (X : ) (Y : ) (X : B) :
(((.obj X✝¹).obj X✝).obj Y).obj X = (X✝¹.obj (X✝.obj X)).obj (Y.obj X)
@[simp]
theorem CategoryTheory.whiskeringRight₂_obj_obj_map_app (B : Type u₁) [] (C : Type u₂) [] (D : Type u₃) [] (E : Type u₄) [] (X : ) (X : ) :
∀ {X_1 Y : } (g : X_1 Y) (X_2 : B), (((.obj X✝).obj X).map g).app X_2 = (X✝.obj (X.obj X_2)).map (g.app X_2)
@[simp]
theorem CategoryTheory.whiskeringRight₂_obj_map_app_app (B : Type u₁) [] (C : Type u₂) [] (D : Type u₃) [] (E : Type u₄) [] (X : ) :
∀ {X_1 Y : } (f : X_1 Y) (Y_1 : ) (X_2 : B), (((.obj X).map f).app Y_1).app X_2 = (X.map (f.app X_2)).app (Y_1.obj X_2)
def CategoryTheory.whiskeringRight₂ (B : Type u₁) [] (C : Type u₂) [] (D : Type u₃) [] (E : Type u₄) [] :

A version of CategoryTheory.whiskeringRight for bifunctors, obtained by uncurrying, applying whiskeringRight and currying back

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Functor.uncurry_obj_curry_obj {B : Type u₁} [] {C : Type u₂} [] {D : Type u₃} [] (F : CategoryTheory.Functor (B × C) D) :
CategoryTheory.uncurry.obj (CategoryTheory.curry.obj F) = F
theorem CategoryTheory.Functor.curry_obj_injective {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] {F₁ : CategoryTheory.Functor (C × D) E} {F₂ : CategoryTheory.Functor (C × D) E} (h : CategoryTheory.curry.obj F₁ = CategoryTheory.curry.obj F₂) :
F₁ = F₂
theorem CategoryTheory.Functor.curry_obj_uncurry_obj {B : Type u₁} [] {C : Type u₂} [] {D : Type u₃} [] (F : ) :
CategoryTheory.curry.obj (CategoryTheory.uncurry.obj F) = F
theorem CategoryTheory.Functor.uncurry_obj_injective {B : Type u₁} [] {C : Type u₂} [] {D : Type u₃} [] {F₁ : } {F₂ : } (h : CategoryTheory.uncurry.obj F₁ = CategoryTheory.uncurry.obj F₂) :
F₁ = F₂
theorem CategoryTheory.Functor.flip_flip {B : Type u₁} [] {C : Type u₂} [] {D : Type u₃} [] (F : ) :
F.flip.flip = F
theorem CategoryTheory.Functor.flip_injective {B : Type u₁} [] {C : Type u₂} [] {D : Type u₃} [] {F₁ : } {F₂ : } (h : F₁.flip = F₂.flip) :
F₁ = F₂
theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip {B : Type u₁} [] {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] {H : Type u₅} [] (F₁ : ) (F₂ : ) (G : CategoryTheory.Functor (C × E) H) :
CategoryTheory.uncurry.obj (F₂.comp (F₁.comp (CategoryTheory.curry.obj G)).flip).flip = (F₁.prod F₂).comp G
theorem CategoryTheory.Functor.uncurry_obj_curry_obj_flip_flip' {B : Type u₁} [] {C : Type u₂} [] {D : Type u₃} [] {E : Type u₄} [] {H : Type u₅} [] (F₁ : ) (F₂ : ) (G : CategoryTheory.Functor (C × E) H) :
CategoryTheory.uncurry.obj (F₁.comp (F₂.comp (CategoryTheory.curry.obj G).flip).flip) = (F₁.prod F₂).comp G