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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

theorem CategoryTheory.NatTrans.app_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C (CategoryTheory.Functor D E)} {G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (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_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C (CategoryTheory.Functor D E)} {G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (Z : D) {X : C} {Y : C} (f : X ⟶ Y) {Z : E} (h : (G.obj Y).obj Z✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.map f).app Z✝) (CategoryTheory.CategoryStruct.comp ((T.app Y).app Z✝) h) = CategoryTheory.CategoryStruct.comp ((T.app X).app Z✝) (CategoryTheory.CategoryStruct.comp ((G.map f).app Z✝) h)

theorem CategoryTheory.NatTrans.naturality_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C (CategoryTheory.Functor D E)} {G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ⟶ G) [∀ (X : C), CategoryTheory.Mono (α.app X)] : CategoryTheory.Mono α

A natural transformation is a monomorphism if each component is.

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

A natural transformation is an epimorphism if each component is.

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

The monoid of natural transformations of the identity is commutative.

@[simp]

theorem CategoryTheory.NatTrans.hcomp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} {I : CategoryTheory.Functor D E} (α : 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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} {I : CategoryTheory.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 := ⋯ }

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Functor.flip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) : CategoryTheory.Functor D (CategoryTheory.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.Iso.map_hom_inv_id_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X : C} {Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (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.Iso.map_hom_inv_id_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X : C} {Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (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.Iso.map_inv_hom_id_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X : C} {Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (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.Iso.map_inv_hom_id_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X : C} {Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (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)

@[deprecated CategoryTheory.Iso.map_hom_inv_id_app]

theorem CategoryTheory.map_hom_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X : C} {Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (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)

Alias of CategoryTheory.Iso.map_hom_inv_id_app.

@[deprecated CategoryTheory.Iso.map_inv_hom_id_app]

theorem CategoryTheory.map_inv_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X : C} {Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (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)

Alias of CategoryTheory.Iso.map_inv_hom_id_app.

@[deprecated CategoryTheory.Iso.map_hom_inv_id_app_assoc]

theorem CategoryTheory.map_hom_inv_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X : C} {Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (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

Alias of CategoryTheory.Iso.map_hom_inv_id_app_assoc.

@[deprecated CategoryTheory.Iso.map_inv_hom_id_app_assoc]

theorem CategoryTheory.map_inv_hom_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {X : C} {Y : C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (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

Alias of CategoryTheory.Iso.map_inv_hom_id_app_assoc.