# mathlib3documentation

category_theory.functor.category

# The category of functors and natural transformations between two fixed categories. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We provide the category instance on C ⥤ D, with morphisms the natural transformations.

## Universes #

If C and D are both small categories at the same universe level, this is another small category at that level. However if C and D are both large categories at the same universe level, this is a small category at the next higher level.

@[protected, instance]
def category_theory.functor.category (C : Type u₁) (D : Type u₂)  :

functor.category C D gives the category structure on functors and natural transformations between categories C and D.

Notice that if C and D are both small categories at the same universe level, this is another small category at that level. However if C and D are both large categories at the same universe level, this is a small category at the next higher level.

Equations
@[simp]
theorem category_theory.nat_trans.vcomp_eq_comp {C : Type u₁} {D : Type u₂} {F G H : C D} (α : F G) (β : G H) :
theorem category_theory.nat_trans.vcomp_app' {C : Type u₁} {D : Type u₂} {F G H : C D} (α : F G) (β : G H) (X : C) :
β).app X = α.app X β.app X
theorem category_theory.nat_trans.congr_app {C : Type u₁} {D : Type u₂} {F G : C D} {α β : F G} (h : α = β) (X : C) :
α.app X = β.app X
@[simp]
theorem category_theory.nat_trans.id_app {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :
(𝟙 F).app X = 𝟙 (F.obj X)
@[simp]
theorem category_theory.nat_trans.comp_app {C : Type u₁} {D : Type u₂} {F G H : C D} (α : F G) (β : G H) (X : C) :
β).app X = α.app X β.app X
theorem category_theory.nat_trans.comp_app_assoc {C : Type u₁} {D : Type u₂} {F G H : C D} (α : F G) (β : G H) (X : C) {X' : D} (f : H.obj X X') :
β).app X f = α.app X β.app X f
theorem category_theory.nat_trans.app_naturality {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D E} (T : F G) (X : C) {Y Z : D} (f : Y Z) :
(F.obj X).map f (T.app X).app Z = (T.app X).app Y (G.obj X).map f
theorem category_theory.nat_trans.naturality_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D E} (T : F G) (Z : D) {X Y : C} (f : X Y) :
(F.map f).app Z (T.app Y).app Z = (T.app X).app Z (G.map f).app Z
theorem category_theory.nat_trans.mono_of_mono_app {C : Type u₁} {D : Type u₂} {F G : C D} (α : F G) [ (X : C), category_theory.mono (α.app X)] :

A natural transformation is a monomorphism if each component is.

theorem category_theory.nat_trans.epi_of_epi_app {C : Type u₁} {D : Type u₂} {F G : C D} (α : F G) [ (X : C), category_theory.epi (α.app X)] :

A natural transformation is an epimorphism if each component is.

def category_theory.nat_trans.hcomp {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D} {H I : D E} (α : F G) (β : H I) :
F H G I

hcomp α β is the horizontal composition of natural transformations.

Equations
@[simp]
theorem category_theory.nat_trans.hcomp_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D} {H I : D E} (α : F G) (β : H I) (X : C) :
β).app X = β.app (F.obj X) I.map (α.app X)
@[simp]
theorem category_theory.nat_trans.hcomp_id_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D} {H : D E} (α : F G) (X : C) :
𝟙 H).app X = H.map (α.app X)
theorem category_theory.nat_trans.id_hcomp_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D} {H : E C} (α : F G) (X : E) :
(𝟙 H α).app X = α.app (H.obj X)
theorem category_theory.nat_trans.exchange {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G H : C D} {I J K : D E} (α : F G) (β : G H) (γ : I J) (δ : J K) :
β) δ) = α γ β δ
@[simp]
theorem category_theory.functor.flip_obj_map {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) (k : D) (j j' : C) (f : j j') :
(F.flip.obj k).map f = (F.map f).app k
@[simp]
theorem category_theory.functor.flip_map_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) (c c' : D) (f : c c') (j : C) :
(F.flip.map f).app j = (F.obj j).map f
@[protected]
def category_theory.functor.flip {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) :
D C E

Flip the arguments of a bifunctor. See also currying.lean.

Equations
@[simp]
theorem category_theory.functor.flip_obj_obj {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) (k : D) (j : C) :
(F.flip.obj k).obj j = (F.obj j).obj k
@[simp]
theorem category_theory.map_hom_inv_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) {X Y : C} (e : X Y) (Z : D) :
(F.map e.hom).app Z (F.map e.inv).app Z = 𝟙 ((F.obj X).obj Z)
@[simp]
theorem category_theory.map_hom_inv_app_assoc {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) {X Y : C} (e : X Y) (Z : D) {X' : E} (f' : (F.obj X).obj Z X') :
(F.map e.hom).app Z (F.map e.inv).app Z f' = f'
@[simp]
theorem category_theory.map_inv_hom_app {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) {X Y : C} (e : X Y) (Z : D) :
(F.map e.inv).app Z (F.map e.hom).app Z = 𝟙 ((F.obj Y).obj Z)
@[simp]
theorem category_theory.map_inv_hom_app_assoc {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D E) {X Y : C} (e : X Y) (Z : D) {X' : E} (f' : (F.obj Y).obj Z X') :
(F.map e.inv).app Z (F.map e.hom).app Z f' = f'