category_theory.functor.currying

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

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

@[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) (T : F ⟶ G) (X : C × D) :

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

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

@[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_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.curry.map T).app X).app Y = T.app (X, Y)

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

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 _

source

@[simp]

theorem category_theory.flip_iso_curry_swap_uncurry_inv_app_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 : D) (X_1 : C) :

((category_theory.flip_iso_curry_swap_uncurry F).inv.app X).app X_1 = 𝟙 ((F.obj X_1).obj X)

source

@[simp]

theorem category_theory.flip_iso_curry_swap_uncurry_hom_app_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 : D) (X_1 : C) :

((category_theory.flip_iso_curry_swap_uncurry F).hom.app X).app X_1 = 𝟙 ((F.obj X_1).obj X)

source

def category_theory.flip_iso_curry_swap_uncurry {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) :

F.flip ≅ category_theory.curry.obj (category_theory.prod.swap D C ⋙ category_theory.uncurry.obj F)

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

Equations

category_theory.flip_iso_curry_swap_uncurry F = category_theory.nat_iso.of_components (λ (d : D), category_theory.nat_iso.of_components (λ (c : C), category_theory.iso.refl ((F.flip.obj d).obj c)) _) _

source

def category_theory.uncurry_obj_flip {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) :

category_theory.uncurry.obj F.flip ≅ category_theory.prod.swap D C ⋙ category_theory.uncurry.obj F

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

Equations

category_theory.uncurry_obj_flip F = category_theory.nat_iso.of_components (λ (p : D × C), category_theory.iso.refl ((category_theory.uncurry.obj F.flip).obj p)) _

source

@[simp]

theorem category_theory.uncurry_obj_flip_inv_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 : D × C) :

(category_theory.uncurry_obj_flip F).inv.app X = 𝟙 ((F.obj X.snd).obj X.fst)

source

@[simp]

theorem category_theory.uncurry_obj_flip_hom_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 : D × C) :

(category_theory.uncurry_obj_flip F).hom.app X = 𝟙 ((F.obj X.snd).obj X.fst)

source

def category_theory.whiskering_right₂ (B : Type u₁) [category_theory.category B] (C : Type u₂) [category_theory.category C] (D : Type u₃) [category_theory.category D] (E : Type u₄) [category_theory.category E] :

(C ⥤ D ⥤ E) ⥤ (B ⥤ C) ⥤ (B ⥤ D) ⥤ B ⥤ E

A version of category_theory.whiskering_right for bifunctors, obtained by uncurrying, applying whiskering_right and currying back

Equations

category_theory.whiskering_right₂ B C D E = category_theory.uncurry ⋙ category_theory.whiskering_right B (C × D) E ⋙ (category_theory.whiskering_left ((B ⥤ C) × (B ⥤ D)) (B ⥤ C × D) (B ⥤ E)).obj (category_theory.prod_functor_to_functor_prod B C D) ⋙ category_theory.curry

source

@[simp]

theorem category_theory.whiskering_right₂_map_app_app_app (B : Type u₁) [category_theory.category B] (C : Type u₂) [category_theory.category C] (D : Type u₃) [category_theory.category D] (E : Type u₄) [category_theory.category E] (_x _x_1 : C ⥤ D ⥤ E) (f : _x ⟶ _x_1) (X : B ⥤ C) (Y : B ⥤ D) (c : B) :

((((category_theory.whiskering_right₂ B C D E).map f).app X).app Y).app c = (f.app (X.obj c)).app (Y.obj c)

source

@[simp]

theorem category_theory.whiskering_right₂_obj_map_app_app (B : Type u₁) [category_theory.category B] (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 X' : B ⥤ C) (f : X_1 ⟶ X') (Y : B ⥤ D) (X_2 : B) :

((((category_theory.whiskering_right₂ B C D E).obj X).map f).app Y).app X_2 = (X.map (f.app X_2)).app (Y.obj X_2)

source

@[simp]

theorem category_theory.whiskering_right₂_obj_obj_obj_obj (B : Type u₁) [category_theory.category B] (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 : B ⥤ C) (Y : B ⥤ D) (X_2 : B) :

((((category_theory.whiskering_right₂ B C D E).obj X).obj X_1).obj Y).obj X_2 = (X.obj (X_1.obj X_2)).obj (Y.obj X_2)

source

@[simp]

theorem category_theory.whiskering_right₂_obj_obj_map_app (B : Type u₁) [category_theory.category B] (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 : B ⥤ C) (Y Y' : B ⥤ D) (g : Y ⟶ Y') (X_2 : B) :

((((category_theory.whiskering_right₂ B C D E).obj X).obj X_1).map g).app X_2 = (X.obj (X_1.obj X_2)).map (g.app X_2)

source

@[simp]

theorem category_theory.whiskering_right₂_obj_obj_obj_map (B : Type u₁) [category_theory.category B] (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 : B ⥤ C) (Y : B ⥤ D) (_x _x_1 : B) (f : _x ⟶ _x_1) :

((((category_theory.whiskering_right₂ B C D E).obj X).obj X_1).obj Y).map f = (X.map (X_1.map f)).app (Y.obj _x) ≫ (X.obj (X_1.obj _x_1)).map (Y.map f)

mathlib3 documentation

Curry and uncurry, as functors. #