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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] : Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (Functor C D)

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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {α β : F ⟶ G} (w : α.app = β.app) : α = β

@[simp]

theorem CategoryTheory.NatTrans.vcomp_eq_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C D} (α : F ⟶ G) (β : G ⟶ H) : vcomp α β = CategoryStruct.comp α β

theorem CategoryTheory.NatTrans.vcomp_app' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : (CategoryStruct.comp α β).app X = CategoryStruct.comp (α.app X) (β.app X)

theorem CategoryTheory.NatTrans.congr_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X

@[simp]

theorem CategoryTheory.NatTrans.id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) : (CategoryStruct.id F).app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.NatTrans.comp_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C) : (CategoryStruct.comp α β).app X = CategoryStruct.comp (α.app X) (β.app X)

theorem CategoryTheory.NatTrans.comp_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C) {Z : D} (h : H.obj X ⟶ Z) : CategoryStruct.comp ((CategoryStruct.comp α β).app X) h = CategoryStruct.comp (α.app X) (CategoryStruct.comp (β.app X) h)

theorem CategoryTheory.NatTrans.app_naturality {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C (Functor D E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) : CategoryStruct.comp ((F.obj X).map f) ((T.app X).app Z) = CategoryStruct.comp ((T.app X).app Y) ((G.obj X).map f)

theorem CategoryTheory.NatTrans.app_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C (Functor D E)} (T : F ⟶ G) (X : C) {Y Z : D} (f : Y ⟶ Z) {Z✝ : E} (h : (G.obj X).obj Z ⟶ Z✝) : CategoryStruct.comp ((F.obj X).map f) (CategoryStruct.comp ((T.app X).app Z) h) = CategoryStruct.comp ((T.app X).app Y) (CategoryStruct.comp ((G.obj X).map f) h)

theorem CategoryTheory.NatTrans.naturality_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C (Functor D E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp ((F.map f).app Z) ((T.app Y).app Z) = CategoryStruct.comp ((T.app X).app Z) ((G.map f).app Z)

theorem CategoryTheory.NatTrans.naturality_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C (Functor D E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y) {Z✝ : E} (h : (G.obj Y).obj Z ⟶ Z✝) : CategoryStruct.comp ((F.map f).app Z) (CategoryStruct.comp ((T.app Y).app Z) h) = CategoryStruct.comp ((T.app X).app Z) (CategoryStruct.comp ((G.map f).app Z) h)

theorem CategoryTheory.NatTrans.naturality_app_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {F G : Functor C (Functor D (Functor E E'))} (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) : CategoryStruct.comp (((F.map f).app X₂).app X₃) (((α.app Y₁).app X₂).app X₃) = CategoryStruct.comp (((α.app X₁).app X₂).app X₃) (((G.map f).app X₂).app X₃)

theorem CategoryTheory.NatTrans.naturality_app_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] {F G : Functor C (Functor D (Functor E E'))} (α : F ⟶ G) {X₁ Y₁ : C} (f : X₁ ⟶ Y₁) (X₂ : D) (X₃ : E) {Z : E'} (h : ((G.obj Y₁).obj X₂).obj X₃ ⟶ Z) : CategoryStruct.comp (((F.map f).app X₂).app X₃) (CategoryStruct.comp (((α.app Y₁).app X₂).app X₃) h) = CategoryStruct.comp (((α.app X₁).app X₂).app X₃) (CategoryStruct.comp (((G.map f).app X₂).app X₃) h)

theorem CategoryTheory.NatTrans.mono_of_mono_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ⟶ G) [∀ (X : C), Mono (α.app X)] : Mono α

A natural transformation is a monomorphism if each component is.

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

A natural transformation is an epimorphism if each component is.

theorem CategoryTheory.NatTrans.id_comm {C : Type u₁} [Category.{v₁, u₁} C] (α β : Functor.id C ⟶ Functor.id C) : CategoryStruct.comp α β = CategoryStruct.comp β α

The monoid of natural transformations of the identity is commutative.

def CategoryTheory.NatTrans.hcomp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} {H I : Functor D E} (α : F ⟶ G) (β : H ⟶ I) : F.comp H ⟶ G.comp I

hcomp α β is the horizontal composition of natural transformations.

Equations

• α ◫ β = { app := fun (X : C) => CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (I.map (α.app X)), naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.hcomp_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} {H I : Functor D E} (α : F ⟶ G) (β : H ⟶ I) (X : C) : (α ◫ β).app X = CategoryStruct.comp (β.app (F.obj X)) (I.map (α.app X))

def CategoryTheory.NatTrans.«term_◫_» : Lean.TrailingParserDescr

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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} {H : Functor D E} (α : F ⟶ G) (X : C) : (α ◫ CategoryStruct.id H).app X = H.map (α.app X)

theorem CategoryTheory.NatTrans.id_hcomp_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} {H : Functor E C} (α : F ⟶ G) (X : E) : (CategoryStruct.id H ◫ α).app X = α.app (H.obj X)

theorem CategoryTheory.NatTrans.exchange {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G H : Functor C D} {I J K : Functor D E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) : CategoryStruct.comp α β ◫ CategoryStruct.comp γ δ = CategoryStruct.comp (α ◫ γ) (β ◫ δ)

def CategoryTheory.Functor.flip {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) : Functor D (Functor 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.Functor.flip_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) (k : D) (j : C) : (F.flip.obj k).obj j = (F.obj j).obj k

@[simp]

theorem CategoryTheory.Functor.flip_obj_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (F.flip.obj k).map f = (F.map f).app k

@[simp]

theorem CategoryTheory.Functor.flip_map_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) : (F.flip.map f).app j = (F.obj j).map f

def CategoryTheory.flipFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] : Functor (Functor C (Functor D E)) (Functor D (Functor C E))

The functor (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E which flips the variables.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.flipFunctor_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : Functor C (Functor D E)) : (flipFunctor C D E).obj F = F.flip

@[simp]

theorem CategoryTheory.flipFunctor_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F₁ F₂ : Functor C (Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C) : (((flipFunctor C D E).map φ).app Y).app X = (φ.app X).app Y

@[simp]

theorem CategoryTheory.Iso.map_hom_inv_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y) (F : Functor C (Functor D E)) (Z : D) : CategoryStruct.comp ((F.map e.hom).app Z) ((F.map e.inv).app Z) = CategoryStruct.id ((F.obj X).obj Z)

@[simp]

theorem CategoryTheory.Iso.map_hom_inv_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y) (F : Functor C (Functor D E)) (Z : D) {Z✝ : E} (h : (F.obj X).obj Z ⟶ Z✝) : CategoryStruct.comp ((F.map e.hom).app Z) (CategoryStruct.comp ((F.map e.inv).app Z) h) = h

@[simp]

theorem CategoryTheory.Iso.map_inv_hom_id_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y) (F : Functor C (Functor D E)) (Z : D) : CategoryStruct.comp ((F.map e.inv).app Z) ((F.map e.hom).app Z) = CategoryStruct.id ((F.obj Y).obj Z)

@[simp]

theorem CategoryTheory.Iso.map_inv_hom_id_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y) (F : Functor C (Functor D E)) (Z : D) {Z✝ : E} (h : (F.obj Y).obj Z ⟶ Z✝) : CategoryStruct.comp ((F.map e.inv).app Z) (CategoryStruct.comp ((F.map e.hom).app Z) h) = h