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] :
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' := _}
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] :
The object level part of the currying functor. (See curry for the functorial version.)
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] :
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' := _}
@[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} :
@[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} :
@[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.is_iso.inv ({app := λ (X_1 : C × D), ((λ (X_1 : C × D), category_theory.eq_to_iso _) X_1).hom, naturality' := _}.app X_1)
@[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_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) :
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] :
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.as_iso (𝟙 ((((𝟭 (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)
@[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_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_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) :
@[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_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_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_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_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 = ((λ (X_1 : C × D), category_theory.eq_to_iso _) X_1).hom