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.

At the end of the file, we provide the left and right unitors, and the associator, for functor composition. (In fact functor composition is definitionally associative, but very often relying on this causes extremely slow elaboration, so it is better to insert it explicitly.)

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₁} [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
  • One or more equations did not get rendered due to their size.
source
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) :
α = β
source
theorem CategoryTheory.NatTrans.ext'_iff {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {α β : F ⟶ G} :
α = β ↔ α.app = β.app
source
@[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 α β
source
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)
source
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
source
@[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)
source
@[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)
source
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)
source
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)
source
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)
source
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)
source
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)
source
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₃)
source
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)
source
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.

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

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

source
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
Instances For
    source
    @[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))
    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₁} [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)
      source
      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)
      source
      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 (α ◫ γ) (β ◫ δ)
      source
      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.
      Instances For
        source
        @[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
        source
        @[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
        source
        @[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
        source
        def CategoryTheory.Functor.leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
        (Functor.id C).comp F ≅ F

        The left unitor, a natural isomorphism ((𝟭 _) ⋙ F) ≅ F.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Functor.leftUnitor_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
          F.leftUnitor.inv.app X = CategoryStruct.id (F.obj X)
          source
          @[simp]
          theorem CategoryTheory.Functor.leftUnitor_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
          F.leftUnitor.hom.app X = CategoryStruct.id (F.obj X)
          source
          def CategoryTheory.Functor.rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
          F.comp (Functor.id D) ≅ F

          The right unitor, a natural isomorphism (F ⋙ (𝟭 B)) ≅ F.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Functor.rightUnitor_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
            F.rightUnitor.inv.app X = CategoryStruct.id (F.obj X)
            source
            @[simp]
            theorem CategoryTheory.Functor.rightUnitor_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : C) :
            F.rightUnitor.hom.app X = CategoryStruct.id (F.obj X)
            source
            def CategoryTheory.Functor.associator {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 : Functor C D) (G : Functor D E) (H : Functor E E') :
            (F.comp G).comp H ≅ F.comp (G.comp H)

            The associator for functors, a natural isomorphism ((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H)).

            (In fact, iso.refl _ will work here, but it tends to make Lean slow later, and it's usually best to insert explicit associators.)

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Functor.associator_inv_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 : Functor C D) (G : Functor D E) (H : Functor E E') (x✝ : C) :
              (F.associator G H).inv.app x✝ = CategoryStruct.id ((F.comp (G.comp H)).obj x✝)
              source
              @[simp]
              theorem CategoryTheory.Functor.associator_hom_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 : Functor C D) (G : Functor D E) (H : Functor E E') (x✝ : C) :
              (F.associator G H).hom.app x✝ = CategoryStruct.id (((F.comp G).comp H).obj x✝)
              source
              theorem CategoryTheory.Functor.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 : Functor C D) (G : Functor D E) (H : Functor E E') :
              (F.comp G).comp H = F.comp (G.comp H)
              source
              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.
              Instances For
                source
                @[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
                source
                @[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
                source
                @[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)
                source
                @[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
                source
                @[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)
                source
                @[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