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₁} [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) :
α = β
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

A natural transformation is a monomorphism if each component is.

A natural transformation is an epimorphism if each component is.

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

hcomp α β is the horizontal composition of natural transformations.

Equations
Instances For

    Notation for horizontal composition of natural transformations.

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

      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
        @[simp]
        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] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {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₁} [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 : 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₁} [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 : 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₁} [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 : 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)