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.

source

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 ⋯ ⋯ ⋯

source

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

α = β

source

@[simp]

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

CategoryTheory.NatTrans.vcomp α β = CategoryTheory.CategoryStruct.comp α β

source

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

(CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)

source

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

α.app X = β.app X

source

@[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)

source

@[simp]

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

(CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)

source

theorem CategoryTheory.NatTrans.comp_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F G 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)

source

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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (X : C) {Y 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)

source

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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (X : C) {Y 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)

source

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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (Z : D) {X 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)

source

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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (Z : D) {X 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)

source

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

CategoryTheory.CategoryStruct.comp (((F.map f).app X₂).app X₃) (((α.app Y₁).app X₂).app X₃) = CategoryTheory.CategoryStruct.comp (((α.app X₁).app X₂).app X₃) (((G.map f).app X₂).app X₃)

source

theorem CategoryTheory.NatTrans.naturality_app_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] {E' : Type u₄} [CategoryTheory.Category.{v₄, u₄} E'] {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.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) :

CategoryTheory.CategoryStruct.comp (((F.map f).app X₂).app X₃) (CategoryTheory.CategoryStruct.comp (((α.app Y₁).app X₂).app X₃) h) = CategoryTheory.CategoryStruct.comp (((α.app X₁).app X₂).app X₃) (CategoryTheory.CategoryStruct.comp (((G.map f).app X₂).app X₃) h)

source

theorem CategoryTheory.NatTrans.mono_of_mono_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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.

source

theorem CategoryTheory.NatTrans.epi_of_epi_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F 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.

source

theorem CategoryTheory.NatTrans.id_comm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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.

source

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 G : CategoryTheory.Functor C D} {H 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 := ⋯ }

Instances For

source

@[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 G : CategoryTheory.Functor C D} {H I : CategoryTheory.Functor D E} (α : F ⟶ G) (β : H ⟶ I) (X : C) :

(α ◫ β).app X = CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (I.map (α.app X))

source

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.

Instances For

source

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 G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} (α : F ⟶ G) (X : C) :

(α ◫ CategoryTheory.CategoryStruct.id H).app X = H.map (α.app X)

source

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 G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor E C} (α : F ⟶ G) (X : E) :

(CategoryTheory.CategoryStruct.id H ◫ α).app X = α.app (H.obj X)

source

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 G H : CategoryTheory.Functor C D} {I J K : CategoryTheory.Functor D E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K) :

CategoryTheory.CategoryStruct.comp α β ◫ CategoryTheory.CategoryStruct.comp γ δ = CategoryTheory.CategoryStruct.comp (α ◫ γ) (β ◫ δ)

source

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.

Instances For

source

@[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

source

@[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

source

@[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

source

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

CategoryTheory.Functor (CategoryTheory.Functor C (CategoryTheory.Functor D E)) (CategoryTheory.Functor D (CategoryTheory.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.

Instances For

source

@[simp]

theorem CategoryTheory.flipFunctor_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)) :

(CategoryTheory.flipFunctor C D E).obj F = F.flip

source

@[simp]

theorem CategoryTheory.flipFunctor_map_app_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₁ F₂ : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C) :

(((CategoryTheory.flipFunctor C D E).map φ).app Y).app X = (φ.app X).app Y

source

@[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 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)

source

@[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 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

source

@[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 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)

source

@[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 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

source

@[deprecated CategoryTheory.Iso.map_hom_inv_id_app (since := "2024-06-09")]

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

source

@[deprecated CategoryTheory.Iso.map_inv_hom_id_app (since := "2024-06-09")]

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

source

@[deprecated CategoryTheory.Iso.map_hom_inv_id_app_assoc (since := "2024-06-09")]

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

source

@[deprecated CategoryTheory.Iso.map_inv_hom_id_app_assoc (since := "2024-06-09")]

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

Documentation

Mathlib.CategoryTheory.Functor.Category

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

Universes #