@[ext]
structure
category_theory.nat_trans
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
- app : Π (X : C), F.obj X ⟶ G.obj X
- naturality' : (∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ c.app Y = c.app X ≫ G.map f) . "obviously"
nat_trans F G represents a natural transformation between functors F and G.
The field app provides the components of the natural transformation.
Naturality is expressed by α.naturality_lemma.
theorem
category_theory.nat_trans.ext
{C : Type u₁}
{_inst_1 : category_theory.category C}
{D : Type u₂}
{_inst_2 : category_theory.category D}
{F G : C ⥤ D}
(x y : category_theory.nat_trans F G) :
theorem
category_theory.nat_trans.ext_iff
{C : Type u₁}
{_inst_1 : category_theory.category C}
{D : Type u₂}
{_inst_2 : category_theory.category D}
{F G : C ⥤ D}
(x y : category_theory.nat_trans F G) :
theorem
category_theory.congr_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
{α β : category_theory.nat_trans F G}
(h : α = β)
(X : C) :
def
category_theory.nat_trans.id
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
nat_trans.id F is the identity natural transformation on a functor F.
Equations
- category_theory.nat_trans.id F = {app := λ (X : C), 𝟙 (F.obj X), naturality' := _}
@[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) :
(category_theory.nat_trans.id F).app X = 𝟙 (F.obj X)
@[instance]
def
category_theory.nat_trans.inhabited
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Equations
def
category_theory.nat_trans.vcomp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G H : C ⥤ D} :
vcomp α β is the vertical compositions of natural transformations.
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}
(α : category_theory.nat_trans F G)
(β : category_theory.nat_trans G H)
(X : C) :