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.
instance
CategoryTheory.Functor.category
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} 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
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)
:
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}
:
@[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)
:
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)
:
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)
:
@[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)
:
@[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)
:
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)
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)
:
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)
@[simp]
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)
:
@[simp]
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)
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)
:
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)
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.
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.
theorem
CategoryTheory.NatTrans.id_comm
{C : Type u₁}
[Category.{v₁, u₁} C]
(α β : Functor.id C ⟶ Functor.id C)
:
The monoid of natural transformations of the identity is commutative.
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)
:
hcomp α β is the horizontal composition of natural transformations.
Equations
Instances For
@[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)
:
Notation for horizontal composition of natural transformations.
Equations
Instances For
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)
:
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)
:
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)
:
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))
:
Flip the arguments of a bifunctor. See also Currying.lean.
Equations
Instances For
@[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)
:
@[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✝)
:
@[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))
{d d' : D}
(f : d ⟶ d')
(c : C)
:
def
CategoryTheory.Functor.leftUnitor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
The left unitor, a natural isomorphism ((𝟭 _) ⋙ F) ≅ F.
Equations
Instances For
@[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)
:
@[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)
:
def
CategoryTheory.Functor.rightUnitor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
The right unitor, a natural isomorphism (F ⋙ (𝟭 B)) ≅ F.
Equations
Instances For
@[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)
:
@[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)
:
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')
:
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
Instances For
@[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)
:
@[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)
:
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')
:
def
CategoryTheory.flipFunctor
(C : Type u₁)
[Category.{v₁, u₁} C]
(D : Type u₂)
[Category.{v₂, u₂} D]
(E : Type u₃)
[Category.{v₃, u₃} E]
:
The functor (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E which flips the variables.
Equations
Instances For
@[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)
:
@[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))
:
@[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)
:
@[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✝)
:
@[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)
:
@[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✝)
: