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.
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)
:
α = β
@[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 α β
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)
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
@[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)
@[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)
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)
:
CategoryStruct.comp ((F.obj X).map f) ((T.app X).app Z) = CategoryStruct.comp ((T.app X).app Y) ((G.obj X).map f)
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)
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)
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)
:
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₃)
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)
:
CategoryStruct.comp α β = CategoryStruct.comp β α
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)
:
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
@[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))
Notation for horizontal composition of natural transformations.
Equations
- One or more equations did not get rendered due to their size.
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)
:
(α ◫ CategoryStruct.id H).app X = H.map (α.app X)
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)
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 (α ◫ γ) (β ◫ δ)
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
- One or more equations did not get rendered due to their size.
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)
:
(F.flip.obj k).obj j = (F.obj j).obj k
@[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
@[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
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
- One or more equations did not get rendered due to their size.
Instances For
@[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
@[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
@[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)
@[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
@[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)
@[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
@[deprecated CategoryTheory.Iso.map_hom_inv_id_app (since := "2024-06-09")]
theorem
CategoryTheory.map_hom_inv_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)
Alias of CategoryTheory.Iso.map_hom_inv_id_app.
@[deprecated CategoryTheory.Iso.map_inv_hom_id_app (since := "2024-06-09")]
theorem
CategoryTheory.map_inv_hom_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)
Alias of CategoryTheory.Iso.map_inv_hom_id_app.
@[deprecated CategoryTheory.Iso.map_hom_inv_id_app_assoc (since := "2024-06-09")]
theorem
CategoryTheory.map_hom_inv_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
@[deprecated CategoryTheory.Iso.map_inv_hom_id_app_assoc (since := "2024-06-09")]
theorem
CategoryTheory.map_inv_hom_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