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₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
:
CategoryTheory.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
- CategoryTheory.Functor.category = CategoryTheory.Category.mk
theorem
CategoryTheory.NatTrans.ext'
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{F : C ⥤ D}
{G : C ⥤ D}
{α : F ⟶ G}
{β : F ⟶ G}
(w : α.app = β.app)
:
α = β
@[simp]
theorem
CategoryTheory.NatTrans.vcomp_eq_comp
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{F : C ⥤ D}
{G : C ⥤ D}
{H : C ⥤ D}
(α : F ⟶ G)
(β : G ⟶ H)
:
CategoryTheory.NatTrans.vcomp α β = α ≫ β
theorem
CategoryTheory.NatTrans.vcomp_app'
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{F : C ⥤ D}
{G : C ⥤ D}
{H : C ⥤ D}
(α : F ⟶ G)
(β : G ⟶ H)
(X : C)
:
theorem
CategoryTheory.NatTrans.congr_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{F : C ⥤ D}
{G : C ⥤ D}
{α : F ⟶ G}
{β : F ⟶ G}
(h : α = β)
(X : C)
:
α.app X = β.app X
@[simp]
theorem
CategoryTheory.NatTrans.id_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
(F : C ⥤ D)
(X : C)
:
@[simp]
theorem
CategoryTheory.NatTrans.comp_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{F : C ⥤ D}
{G : C ⥤ D}
{H : C ⥤ D}
(α : F ⟶ G)
(β : G ⟶ H)
(X : C)
:
theorem
CategoryTheory.NatTrans.app_naturality
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
{F : C ⥤ D ⥤ E}
{G : C ⥤ D ⥤ E}
(T : F ⟶ G)
(X : C)
{Y : D}
{Z : D}
(f : Y ⟶ Z)
:
theorem
CategoryTheory.NatTrans.naturality_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
{F : C ⥤ D ⥤ E}
{G : C ⥤ D ⥤ E}
(T : F ⟶ G)
(Z : D)
{X : C}
{Y : C}
(f : X ⟶ Y)
:
theorem
CategoryTheory.NatTrans.mono_of_mono_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{F : C ⥤ D}
{G : C ⥤ D}
(α : F ⟶ G)
[inst : ∀ (X : C), CategoryTheory.Mono (α.app X)]
:
A natural transformation is a monomorphism if each component is.
theorem
CategoryTheory.NatTrans.epi_of_epi_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{F : C ⥤ D}
{G : C ⥤ D}
(α : F ⟶ G)
[inst : ∀ (X : C), CategoryTheory.Epi (α.app X)]
:
A natural transformation is an epimorphism if each component is.
@[simp]
theorem
CategoryTheory.NatTrans.hcomp_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
{F : C ⥤ D}
{G : C ⥤ D}
{H : D ⥤ E}
{I : D ⥤ E}
(α : F ⟶ G)
(β : H ⟶ I)
(X : C)
:
def
CategoryTheory.NatTrans.hcomp
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
{F : C ⥤ D}
{G : C ⥤ D}
{H : D ⥤ E}
{I : D ⥤ E}
(α : F ⟶ G)
(β : H ⟶ I)
:
hcomp α β is the horizontal composition of natural transformations.
Equations
- α ◫ β = CategoryTheory.NatTrans.mk fun X => β.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.
theorem
CategoryTheory.NatTrans.hcomp_id_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
{F : C ⥤ D}
{G : C ⥤ D}
{H : D ⥤ E}
(α : F ⟶ G)
(X : C)
:
theorem
CategoryTheory.NatTrans.id_hcomp_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
{F : C ⥤ D}
{G : C ⥤ D}
{H : E ⥤ C}
(α : F ⟶ G)
(X : E)
:
theorem
CategoryTheory.NatTrans.exchange
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
{F : C ⥤ D}
{G : C ⥤ D}
{H : C ⥤ D}
{I : D ⥤ E}
{J : D ⥤ E}
{K : D ⥤ E}
(α : F ⟶ G)
(β : G ⟶ H)
(γ : I ⟶ J)
(δ : J ⟶ K)
:
@[simp]
theorem
CategoryTheory.Functor.flip_obj_map
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
(F : C ⥤ D ⥤ E)
(k : D)
:
∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Functor.flip F).obj k).map f = (F.map f).app k
@[simp]
theorem
CategoryTheory.Functor.flip_map_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
(F : C ⥤ D ⥤ E)
:
∀ {X Y : D} (f : X ⟶ Y) (j : C), ((CategoryTheory.Functor.flip F).map f).app j = (F.obj j).map f
@[simp]
theorem
CategoryTheory.Functor.flip_obj_obj
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
(F : C ⥤ D ⥤ E)
(k : D)
(j : C)
:
((CategoryTheory.Functor.flip F).obj k).obj j = (F.obj j).obj k
def
CategoryTheory.Functor.flip
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
(F : C ⥤ 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.
@[simp]
theorem
CategoryTheory.map_hom_inv_app_assoc
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
(F : C ⥤ D ⥤ E)
{X : C}
{Y : C}
(e : X ≅ Y)
(Z : D)
{Z : E}
(h : (F.obj X).obj Z ⟶ Z)
:
@[simp]
theorem
CategoryTheory.map_hom_inv_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
(F : C ⥤ D ⥤ E)
{X : C}
{Y : C}
(e : X ≅ Y)
(Z : D)
:
@[simp]
theorem
CategoryTheory.map_inv_hom_app_assoc
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
(F : C ⥤ D ⥤ E)
{X : C}
{Y : C}
(e : X ≅ Y)
(Z : D)
{Z : E}
(h : (F.obj Y).obj Z ⟶ Z)
:
@[simp]
theorem
CategoryTheory.map_inv_hom_app
{C : Type u₁}
[inst : CategoryTheory.Category C]
{D : Type u₂}
[inst : CategoryTheory.Category D]
{E : Type u₃}
[inst : CategoryTheory.Category E]
(F : C ⥤ D ⥤ E)
{X : C}
{Y : C}
(e : X ≅ Y)
(Z : D)
: