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.

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
  • CategoryTheory.Functor.category = CategoryTheory.Category.mk
theorem CategoryTheory.NatTrans.ext' {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} {G : C D} {α : F G} {β : F G} (w : α.app = β.app) :
α = β
@[simp]
theorem CategoryTheory.NatTrans.vcomp_eq_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} {G : C D} {H : C D} (α : F G) (β : G H) :
theorem CategoryTheory.NatTrans.vcomp_app' {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} {G : C D} {H : C D} (α : F G) (β : G H) (X : C) :
(α β).app X = α.app X β.app X
theorem CategoryTheory.NatTrans.congr_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} {G : C D} {α : F G} {β : F G} (h : α = β) (X : C) :
α.app X = β.app X
@[simp]
theorem CategoryTheory.NatTrans.id_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) (X : C) :
(𝟙 F).app X = 𝟙 (F.obj X)
@[simp]
theorem CategoryTheory.NatTrans.comp_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} {G : C D} {H : C D} (α : F G) (β : G H) (X : C) :
(α β).app X = α.app X β.app X
theorem CategoryTheory.NatTrans.app_naturality {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D E} {G : C D E} (T : F G) (X : C) {Y : D} {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 CategoryTheory.NatTrans.naturality_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D E} {G : C D E} (T : F G) (Z : D) {X : C} {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 CategoryTheory.NatTrans.mono_of_mono_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} {G : C D} (α : F G) [inst : ∀ (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₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} {G : C D} (α : F G) [inst : ∀ (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₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : C D} {H : D E} {I : D E} (α : F G) (β : H I) (X : C) :
(α β).app X = β.app (F.obj X) I.map (α.app X)
def CategoryTheory.NatTrans.hcomp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : C D} {H : D E} {I : D E} (α : F G) (β : H I) :
F H G I

hcomp α β is the horizontal composition of natural transformations.

Equations

Notation for horizontal composition of natural transformations.

Equations
  • One or more equations did not get rendered due to their size.
theorem CategoryTheory.NatTrans.hcomp_id_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : C D} {H : D E} (α : F G) (X : C) :
(α 𝟙 H).app X = H.map (α.app X)
theorem CategoryTheory.NatTrans.id_hcomp_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : C D} {H : E C} (α : F G) (X : E) :
(𝟙 H α).app X = α.app (H.obj X)
theorem CategoryTheory.NatTrans.exchange {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : C D} {H : C D} {I : D E} {J : D E} {K : D E} (α : F G) (β : G H) (γ : I J) (δ : J K) :
(α β) (γ δ) = (α γ) β δ
@[simp]
theorem CategoryTheory.Functor.flip_obj_map {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D E) (k : D) :
∀ {X Y : C} (f : X Y), ((CategoryTheory.Functor.flip F).obj k).map f = (F.map f).app k
@[simp]
theorem CategoryTheory.Functor.flip_map_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D E) :
∀ {X Y : D} (f : X Y) (j : C), ((CategoryTheory.Functor.flip F).map f).app j = (F.obj j).map f
@[simp]
theorem CategoryTheory.Functor.flip_obj_obj {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D E) (k : D) (j : C) :
((CategoryTheory.Functor.flip F).obj k).obj j = (F.obj j).obj k
def CategoryTheory.Functor.flip {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D E) :
D C E

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.map_hom_inv_app_assoc {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D E) {X : C} {Y : C} (e : X Y) (Z : D) {Z : E} (h : (F.obj X).obj Z Z) :
(F.map e.hom).app Z (F.map e.inv).app Z h = h
@[simp]
theorem CategoryTheory.map_hom_inv_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D E) {X : C} {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 CategoryTheory.map_inv_hom_app_assoc {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D E) {X : C} {Y : C} (e : X Y) (Z : D) {Z : E} (h : (F.obj Y).obj Z Z) :
(F.map e.inv).app Z (F.map e.hom).app Z h = h
@[simp]
theorem CategoryTheory.map_inv_hom_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D E) {X : C} {Y : C} (e : X Y) (Z : D) :
(F.map e.inv).app Z (F.map e.hom).app Z = 𝟙 ((F.obj Y).obj Z)