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.
@[protected, instance]
def
category_theory.functor.category
(C : Type u₁)
[category_theory.category C]
(D : Type u₂)
[category_theory.category D] :
category_theory.category (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
- category_theory.functor.category C D = {to_category_struct := {to_quiver := {hom := λ (F G : C ⥤ D), category_theory.nat_trans F G}, id := λ (F : C ⥤ D), category_theory.nat_trans.id F, comp := λ (_x _x_1 _x_2 : C ⥤ D) (α : _x ⟶ _x_1) (β : _x_1 ⟶ _x_2), category_theory.nat_trans.vcomp α β}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
theorem
category_theory.nat_trans.vcomp_eq_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G H : C ⥤ D}
(α : F ⟶ G)
(β : G ⟶ H) :
category_theory.nat_trans.vcomp α β = α ≫ β
theorem
category_theory.nat_trans.vcomp_app'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G H : C ⥤ D}
(α : F ⟶ G)
(β : G ⟶ H)
(X : C) :
theorem
category_theory.nat_trans.congr_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
{α β : F ⟶ G}
(h : α = β)
(X : C) :
@[simp]
theorem
category_theory.nat_trans.id_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
(X : C) :
@[simp]
theorem
category_theory.nat_trans.comp_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G H : C ⥤ D}
(α : F ⟶ G)
(β : G ⟶ H)
(X : C) :
theorem
category_theory.nat_trans.app_naturality
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{F G : C ⥤ D ⥤ E}
(T : F ⟶ G)
(X : C)
{Y Z : D}
(f : Y ⟶ Z) :
theorem
category_theory.nat_trans.naturality_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{F G : C ⥤ D ⥤ E}
(T : F ⟶ G)
(Z : D)
{X Y : C}
(f : X ⟶ Y) :
theorem
category_theory.nat_trans.mono_app_of_mono
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ⟶ G)
[∀ (X : C), category_theory.mono (α.app X)] :
A natural transformation is a monomorphism if each component is.
theorem
category_theory.nat_trans.epi_app_of_epi
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ⟶ G)
[∀ (X : C), category_theory.epi (α.app X)] :
A natural transformation is an epimorphism if each component is.
def
category_theory.nat_trans.hcomp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{F G : C ⥤ D}
{H I : D ⥤ E}
(α : F ⟶ G)
(β : H ⟶ I) :
hcomp α β is the horizontal composition of natural transformations.
@[simp]
theorem
category_theory.nat_trans.hcomp_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{F G : C ⥤ D}
{H I : D ⥤ E}
(α : F ⟶ G)
(β : H ⟶ I)
(X : C) :
@[simp]
theorem
category_theory.nat_trans.hcomp_id_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{F G : C ⥤ D}
{H : D ⥤ E}
(α : F ⟶ G)
(X : C) :
theorem
category_theory.nat_trans.id_hcomp_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{F G : C ⥤ D}
{H : E ⥤ C}
(α : F ⟶ G)
(X : E) :
theorem
category_theory.nat_trans.exchange
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
{F G H : C ⥤ D}
{I J K : D ⥤ E}
(α : F ⟶ G)
(β : G ⟶ H)
(γ : I ⟶ J)
(δ : J ⟶ K) :
@[protected]
def
category_theory.functor.flip
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E) :
Flip the arguments of a bifunctor. See also currying.lean.
@[simp]
theorem
category_theory.functor.flip_obj_obj
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
(c : C)
(d : D) :
@[simp]
theorem
category_theory.functor.flip_obj_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
{c c' : C}
(f : c ⟶ c')
(d : D) :
@[simp]
theorem
category_theory.functor.flip_map_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
{d d' : D}
(f : d ⟶ d')
(c : C) :
@[simp]
theorem
category_theory.map_hom_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
{X Y : C}
(e : X ≅ Y)
(Z : D) :
@[simp]
theorem
category_theory.map_hom_inv_app_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
{X Y : C}
(e : X ≅ Y)
(Z : D)
{X' : E}
(f' : (F.obj X).obj Z ⟶ X') :
@[simp]
theorem
category_theory.map_inv_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
{X Y : C}
(e : X ≅ Y)
(Z : D) :
@[simp]
theorem
category_theory.map_inv_hom_app_assoc
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D ⥤ E)
{X Y : C}
(e : X ≅ Y)
(Z : D)
{X' : E}
(f' : (F.obj Y).obj Z ⟶ X') :