# Documentation

Mathlib.CategoryTheory.Functor.Category

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

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.

instance CategoryTheory.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.

theorem CategoryTheory.NatTrans.ext' {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {α : F G} {β : F G} (w : α.app = β.app) :
α = β
@[simp]
theorem CategoryTheory.NatTrans.vcomp_eq_comp {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (α : F G) (β : G H) :
theorem CategoryTheory.NatTrans.vcomp_app' {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (α : F G) (β : G H) (X : C) :
().app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
theorem CategoryTheory.NatTrans.congr_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {α : F G} {β : F G} (h : α = β) (X : C) :
α.app X = β.app X
@[simp]
theorem CategoryTheory.NatTrans.id_app {C : Type u₁} [] {D : Type u₂} [] (F : ) (X : C) :
@[simp]
theorem CategoryTheory.NatTrans.comp_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (α : F G) (β : G H) (X : C) :
().app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
theorem CategoryTheory.NatTrans.comp_app_assoc {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } (α : F G) (β : G H) (X : C) {Z : D} (h : H.obj X Z) :
theorem CategoryTheory.NatTrans.app_naturality {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } (T : F G) (X : C) {Y : D} {Z : D} (f : Y Z) :
CategoryTheory.CategoryStruct.comp ((F.obj X).map f) ((T.app X).app Z) = CategoryTheory.CategoryStruct.comp ((T.app X).app Y) ((G.obj X).map f)
theorem CategoryTheory.NatTrans.naturality_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } (T : F G) (Z : D) {X : C} {Y : C} (f : X Y) :
CategoryTheory.CategoryStruct.comp ((F.map f).app Z) ((T.app Y).app Z) = CategoryTheory.CategoryStruct.comp ((T.app X).app Z) ((G.map f).app Z)
theorem CategoryTheory.NatTrans.mono_of_mono_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) [∀ (X : C), CategoryTheory.Mono (α.app X)] :

A natural transformation is a monomorphism if each component is.

theorem CategoryTheory.NatTrans.epi_of_epi_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) [∀ (X : C), CategoryTheory.Epi (α.app X)] :

A natural transformation is an epimorphism if each component is.

@[simp]
theorem CategoryTheory.NatTrans.hcomp_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {I : } (α : F G) (β : H I) (X : C) :
(α β).app X = CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (I.map (α.app X))
def CategoryTheory.NatTrans.hcomp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {I : } (α : F G) (β : H I) :

hcomp α β is the horizontal composition of natural transformations.

Instances For

Notation for horizontal composition of natural transformations.

Instances For
theorem CategoryTheory.NatTrans.hcomp_id_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (α : F G) (X : C) :
().app X = H.map (α.app X)
theorem CategoryTheory.NatTrans.id_hcomp_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (α : F G) (X : E) :
().app X = α.app (H.obj X)
theorem CategoryTheory.NatTrans.exchange {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } {I : } {J : } {K : } (α : F G) (β : G H) (γ : I J) (δ : J K) :
@[simp]
theorem CategoryTheory.Functor.flip_obj_map {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (k : D) :
∀ {X Y : C} (f : X Y), (().obj k).map f = (F.map f).app k
@[simp]
theorem CategoryTheory.Functor.flip_map_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) :
∀ {X Y : D} (f : X Y) (j : C), (().map f).app j = (F.obj j).map f
@[simp]
theorem CategoryTheory.Functor.flip_obj_obj {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (k : D) (j : C) :
(().obj k).obj j = (F.obj j).obj k
def CategoryTheory.Functor.flip {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) :

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

Instances For
@[simp]
theorem CategoryTheory.map_hom_inv_app_assoc {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) {X : C} {Y : C} (e : X Y) (Z : D) {Z : E} (h : (F.obj X).obj Z Z) :
CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) (CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) h) = h
@[simp]
theorem CategoryTheory.map_hom_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) {X : C} {Y : C} (e : X Y) (Z : D) :
CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) ((F.map e.inv).app Z) = CategoryTheory.CategoryStruct.id ((F.obj X).obj Z)
@[simp]
theorem CategoryTheory.map_inv_hom_app_assoc {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) {X : C} {Y : C} (e : X Y) (Z : D) {Z : E} (h : (F.obj Y).obj Z Z) :
CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) (CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) h) = h
@[simp]
theorem CategoryTheory.map_inv_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) {X : C} {Y : C} (e : X Y) (Z : D) :
CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) ((F.map e.hom).app Z) = CategoryTheory.CategoryStruct.id ((F.obj Y).obj Z)