category_theory.currying

source

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

category_theory.uncurry = {obj := λ (F : C ⥤ D ⥤ E), {obj := λ (X : C × D), (F.obj X.fst).obj X.snd, map := λ (X Y : C × D) (f : X ⟶ Y), (F.map f.fst).app X.snd ≫ (F.obj Y.fst).map f.snd, map_id' := _, map_comp' := _}, map := λ (F G : C ⥤ D ⥤ E) (T : F ⟶ G), {app := λ (X : C × D), (T.app X.fst).app X.snd, naturality' := _}, map_id' := _, map_comp' := _}

source

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] (F : C × D ⥤ E) :

C ⥤ D ⥤ E

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

Equations

category_theory.curry_obj F = {obj := λ (X : C), {obj := λ (Y : D), F.obj (X, Y), map := λ (Y Y' : D) (g : Y ⟶ Y'), F.map (𝟙 X, g), map_id' := _, map_comp' := _}, map := λ (X X' : C) (f : X ⟶ X'), {app := λ (Y : D), F.map (f, 𝟙 Y), naturality' := _}, map_id' := _, map_comp' := _}

source

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

category_theory.curry = {obj := λ (F : C × D ⥤ E), category_theory.curry_obj F, map := λ (F G : C × D ⥤ E) (T : F ⟶ G), {app := λ (X : C), {app := λ (Y : D), T.app (X, Y), naturality' := _}, naturality' := _}, map_id' := _, map_comp' := _}

source

@[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} :

(category_theory.uncurry.obj F).obj X = (F.obj X.fst).obj X.snd

source

@[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} :

(category_theory.uncurry.obj F).map f = (F.map f.fst).app X.snd ≫ (F.obj Y.fst).map f.snd

source

@[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} :

(category_theory.uncurry.map α).app X = (α.app X.fst).app X.snd

source

@[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)

source

@[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'} :

((category_theory.curry.obj F).obj X).map g = F.map (𝟙 X, g)

source

@[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} :

((category_theory.curry.obj F).map f).app Y = F.map (f, 𝟙 Y)

source

@[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)

source

@[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) :

((category_theory.currying.inverse.map T).app X).app Y = T.app (X, Y)

source

@[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) :

((category_theory.currying.inverse.obj F).map f).app Y = F.map (f, 𝟙 Y)

source

@[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) :

(category_theory.currying.counit_iso.hom.app X).app X_1 = category_theory.eq_to_hom _

source

@[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.iso.refl ((category_theory.uncurry.obj X).obj ((X_1, X_2).fst, (X_1, X_2).snd))).inv

source

@[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) :

(category_theory.currying.functor.obj F).obj X = (F.obj X.fst).obj X.snd

source

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

category_theory.currying = category_theory.equivalence.mk category_theory.uncurry category_theory.curry (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.iso.refl ((((𝟭 (C ⥤ D ⥤ E)).obj F).obj X).obj Y)) _) _) category_theory.currying._proof_3) (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)

source

@[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) :

((category_theory.currying.inverse.obj F).obj X).obj Y = F.obj (X, Y)

source

@[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) :

(category_theory.currying.functor.map T).app X = (T.app X.fst).app X.snd

source

@[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') :

((category_theory.currying.inverse.obj F).obj X).map g = F.map (𝟙 X, g)

source

@[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 = 𝟙 ((X.obj X_1).obj X_2)

source

@[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) :

(category_theory.currying.functor.obj F).map f = (F.map f.fst).app X.snd ≫ (F.obj Y.fst).map f.snd

source

@[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) :

(category_theory.currying.counit_iso.inv.app X).app X_1 = category_theory.eq_to_hom _

mathlib documentation

Curry and uncurry, as functors. #