# mathlibdocumentation

category_theory.natural_transformation

# Natural transformations #

Defines natural transformations between functors.

A natural transformation α : nat_trans F G consists of morphisms α.app X : F.obj X ⟶ G.obj X, and the naturality squares α.naturality f : F.map f ≫ α.app Y = α.app X ≫ G.map f, where f : X ⟶ Y.

Note that we make nat_trans.naturality a simp lemma, with the preferred simp normal form pushing components of natural transformations to the left.

See also category_theory.functor_category, where we provide the category structure on functors and natural transformations.

Introduces notations

• τ.app X for the components of natural transformations,
• F ⟶ G for the type of natural transformations between functors F and G (this and the next require category_theory.functor_category),
• σ ≫ τ for vertical compositions, and
• σ ◫ τ for horizontal compositions.
@[ext]
structure category_theory.nat_trans {C : Type u₁} {D : Type u₂} (F G : C D) :
Type (max u₁ v₂)

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 : G) (h : x.app = y.app) :
x = y
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 : G) :
x = y x.app = y.app
@[simp]
theorem category_theory.nat_trans.naturality {C : Type u₁} {D : Type u₂} {F G : C D} (self : G) ⦃X Y : C⦄ (f : X Y) :
F.map f self.app Y = self.app X G.map f
@[simp]
theorem category_theory.nat_trans.naturality_assoc {C : Type u₁} {D : Type u₂} {F G : C D} (self : G) ⦃X Y : C⦄ (f : X Y) {X' : D} (f' : G.obj Y X') :
F.map f self.app Y f' = self.app X G.map f f'
theorem category_theory.congr_app {C : Type u₁} {D : Type u₂} {F G : C D} {α β : G} (h : α = β) (X : C) :
α.app X = β.app X
def category_theory.nat_trans.id {C : Type u₁} {D : Type u₂} (F : C D) :

nat_trans.id F is the identity natural transformation on a functor F.

Equations
@[simp]
theorem category_theory.nat_trans.id_app' {C : Type u₁} {D : Type u₂} (F : C D) (X : C) :
= 𝟙 (F.obj X)
@[instance]
def category_theory.nat_trans.inhabited {C : Type u₁} {D : Type u₂} (F : C D) :
Equations
def category_theory.nat_trans.vcomp {C : Type u₁} {D : Type u₂} {F G H : C D} (α : G) (β : H) :

vcomp α β is the vertical compositions of natural transformations.

Equations
theorem category_theory.nat_trans.vcomp_app {C : Type u₁} {D : Type u₂} {F G H : C D} (α : G) (β : H) (X : C) :
(α.vcomp β).app X = α.app X β.app X