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

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

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