mathlib documentation

category_theory.currying

def category_theory.uncurry {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] :
(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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] :
C × D EC D E

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

Equations
def category_theory.curry {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] :
(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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C D E} {X : C × D} :

@[simp]
theorem category_theory.uncurry.obj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C D E} {X Y : C × D} {f : X Y} :

@[simp]
theorem category_theory.uncurry.map_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C D E} {α : F G} {X : C × D} :

@[simp]
theorem category_theory.curry.obj_obj_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C × D E} {X : C} {Y : D} :
((category_theory.curry.obj F).obj X).obj Y = F.obj (X, Y)

@[simp]
theorem category_theory.curry.obj_obj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C × D E} {X : C} {Y Y' : D} {g : Y Y'} :

@[simp]
theorem category_theory.curry.obj_map_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C × D E} {X X' : C} {f : X X'} {Y : D} :

@[simp]
theorem category_theory.curry.map_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C × D E} {α : F G} {X : C} {Y : D} :
((category_theory.curry.map α).app X).app Y = α.app (X, Y)

@[simp]
theorem category_theory.currying_inverse_map_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F G : C × D E) (T : F G) (X : C) (Y : D) :

@[simp]
theorem category_theory.currying_inverse_obj_map_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C × D E) (X X' : C) (f : X X') (Y : D) :

@[simp]
theorem category_theory.currying_counit_iso_hom_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (X : C × D E) (X_1 : C × D) :

@[simp]
theorem category_theory.currying_unit_iso_hom_app_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (X : C D E) (X_1 : C) (X_2 : D) :
((category_theory.currying.unit_iso.hom.app X).app X_1).app X_2 = (((((((category_theory.nat_iso.of_components (λ (F : C D E), category_theory.nat_iso.of_components (λ (X : C), category_theory.nat_iso.of_components (λ (Y : D), category_theory.as_iso (𝟙 ((((𝟭 (C D E)).obj F).obj X).obj Y))) _) _) category_theory.currying._proof_3 ≪≫ category_theory.iso_whisker_left category_theory.uncurry category_theory.curry.left_unitor.symm) ≪≫ category_theory.iso_whisker_left category_theory.uncurry (category_theory.iso_whisker_right (category_theory.nat_iso.of_components (λ (F : C × D E), category_theory.nat_iso.of_components (λ (X : C × D), category_theory.eq_to_iso _) _) category_theory.currying._proof_6).symm category_theory.curry)) ≪≫ category_theory.iso_whisker_left category_theory.uncurry (category_theory.curry.associator category_theory.uncurry category_theory.curry)) ≪≫ (category_theory.uncurry.associator category_theory.curry (category_theory.uncurry category_theory.curry)).symm) ≪≫ category_theory.iso_whisker_right (category_theory.nat_iso.of_components (λ (F : C D E), category_theory.nat_iso.of_components (λ (X : C), category_theory.nat_iso.of_components (λ (Y : D), category_theory.as_iso (𝟙 ((((𝟭 (C D E)).obj F).obj X).obj Y))) _) _) category_theory.currying._proof_3).symm (category_theory.uncurry category_theory.curry)).hom.app X).app X_1).app X_2 (((category_theory.uncurry category_theory.curry).left_unitor.hom.app X).app X_1).app X_2

@[simp]
theorem category_theory.currying_functor_obj_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D E) (X : C × D) :

def category_theory.currying {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] :
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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C × D E) (X : C) (Y : D) :

@[simp]
theorem category_theory.currying_functor_map_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F G : C D E) (T : F G) (X : C × D) :

@[simp]
theorem category_theory.currying_inverse_obj_obj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C × D E) (X : C) (Y Y' : D) (g : Y Y') :

@[simp]
theorem category_theory.currying_unit_iso_inv_app_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (X : C D E) (X_1 : C) (X_2 : D) :
((category_theory.currying.unit_iso.inv.app X).app X_1).app X_2 = (((category_theory.uncurry category_theory.curry).left_unitor.inv.app X).app X_1).app X_2 (((((((category_theory.nat_iso.of_components (λ (F : C D E), category_theory.nat_iso.of_components (λ (X : C), category_theory.nat_iso.of_components (λ (Y : D), category_theory.as_iso (𝟙 ((((𝟭 (C D E)).obj F).obj X).obj Y))) _) _) category_theory.currying._proof_3 ≪≫ category_theory.iso_whisker_left category_theory.uncurry category_theory.curry.left_unitor.symm) ≪≫ category_theory.iso_whisker_left category_theory.uncurry (category_theory.iso_whisker_right (category_theory.nat_iso.of_components (λ (F : C × D E), category_theory.nat_iso.of_components (λ (X : C × D), category_theory.eq_to_iso _) _) category_theory.currying._proof_6).symm category_theory.curry)) ≪≫ category_theory.iso_whisker_left category_theory.uncurry (category_theory.curry.associator category_theory.uncurry category_theory.curry)) ≪≫ (category_theory.uncurry.associator category_theory.curry (category_theory.uncurry category_theory.curry)).symm) ≪≫ category_theory.iso_whisker_right (category_theory.nat_iso.of_components (λ (F : C D E), category_theory.nat_iso.of_components (λ (X : C), category_theory.nat_iso.of_components (λ (Y : D), category_theory.as_iso (𝟙 ((((𝟭 (C D E)).obj F).obj X).obj Y))) _) _) category_theory.currying._proof_3).symm (category_theory.uncurry category_theory.curry)).inv.app X).app X_1).app X_2

@[simp]
theorem category_theory.currying_functor_obj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D E) (X Y : C × D) (f : X Y) :

@[simp]
theorem category_theory.currying_counit_iso_inv_app_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (X : C × D E) (X_1 : C × D) :