# mathlibdocumentation

category_theory.currying

# 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).

def category_theory.uncurry {C : Type u₁} {D : Type u₂} {E : Type u₃}  :
(C D E) C × D E

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

Equations
def category_theory.curry_obj {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C × D E) :
C D E

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

Equations
def category_theory.curry {C : Type u₁} {D : Type u₂} {E : Type u₃}  :
(C × D E) C D E

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

Equations
@[simp]
theorem category_theory.uncurry.obj_obj {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C D E} {X : C × D} :
= (F.obj X.fst).obj X.snd
@[simp]
theorem category_theory.uncurry.obj_map {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C D E} {X Y : C × D} {f : X Y} :
= (F.map f.fst).app X.snd (F.obj Y.fst).map f.snd
@[simp]
theorem category_theory.uncurry.map_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D E} {α : F G} {X : C × D} :
= (α.app X.fst).app X.snd
@[simp]
theorem category_theory.curry.obj_obj_obj {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C × D E} {X : C} {Y : D} :
.obj X).obj Y = F.obj (X, Y)
@[simp]
theorem category_theory.curry.obj_obj_map {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C × D E} {X : C} {Y Y' : D} {g : Y Y'} :
.obj X).map g = F.map (𝟙 X, g)
@[simp]
theorem category_theory.curry.obj_map_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C × D E} {X X' : C} {f : X X'} {Y : D} :
.map f).app Y = F.map (f, 𝟙 Y)
@[simp]
theorem category_theory.curry.map_app_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C × D E} {α : F G} {X : C} {Y : D} :
.app X).app Y = α.app (X, Y)
@[simp]
theorem category_theory.currying_inverse_map_app_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (F G : C × D E) (T : F G) (X : C) (Y : D) :
X).app Y = T.app (X, Y)
@[simp]
theorem category_theory.currying_inverse_obj_map_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C × D E) (X X' : C) (f : X X') (Y : D) :
f).app Y = F.map (f, 𝟙 Y)
@[simp]
theorem category_theory.currying_counit_iso_hom_app_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (X : C × D E) (X_1 : C × D) :
@[simp]
theorem category_theory.currying_unit_iso_hom_app_app_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (X : C D E) (X_1 : C) (X_2 : D) :
X_1).app X_2 = (category_theory.iso.refl ((X_1, X_2).fst, (X_1, X_2).snd))).inv
@[simp]
theorem category_theory.currying_functor_obj_obj {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) (X : C × D) :
= (F.obj X.fst).obj X.snd
def category_theory.currying {C : Type u₁} {D : Type u₂} {E : Type u₃}  :
C D E C × D E

The equivalence of functor categories given by currying/uncurrying.

Equations
@[simp]
theorem category_theory.currying_inverse_obj_obj_obj {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C × D E) (X : C) (Y : D) :
X).obj Y = F.obj (X, Y)
@[simp]
theorem category_theory.currying_functor_map_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (F G : C D E) (T : F G) (X : C × D) :
= (T.app X.fst).app X.snd
@[simp]
theorem category_theory.currying_inverse_obj_obj_map {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C × D E) (X : C) (Y Y' : D) (g : Y Y') :
X).map g = F.map (𝟙 X, g)
@[simp]
theorem category_theory.currying_unit_iso_inv_app_app_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (X : C D E) (X_1 : C) (X_2 : D) :
X_1).app X_2 = 𝟙 ((X.obj X_1).obj X_2)
@[simp]
theorem category_theory.currying_functor_obj_map {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) (X Y : C × D) (f : X Y) :
= (F.map f.fst).app X.snd (F.obj Y.fst).map f.snd
@[simp]
theorem category_theory.currying_counit_iso_inv_app_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (X : C × D E) (X_1 : C × D) :
@[simp]
theorem category_theory.flip_iso_curry_swap_uncurry_inv_app_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) (X : D) (X_1 : C) :
X_1 = 𝟙 ((F.obj X_1).obj X)
@[simp]
theorem category_theory.flip_iso_curry_swap_uncurry_hom_app_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) (X : D) (X_1 : C) :
X_1 = 𝟙 ((F.obj X_1).obj X)
def category_theory.flip_iso_curry_swap_uncurry {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) :

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

Equations