mathlib documentation

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

@[ext]
structure category_theory.nat_trans {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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 : category_theory.nat_trans F 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 : category_theory.nat_trans F G) :
x = y x.app = y.app
@[simp]
theorem category_theory.nat_trans.naturality {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C D} (self : category_theory.nat_trans F 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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C D} (self : category_theory.nat_trans F 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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C D} {α β : category_theory.nat_trans F G} (h : α = β) (X : C) :
α.app X = β.app X
@[protected]

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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) (X : C) :

vcomp α β is the vertical compositions of natural transformations.

Equations
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) :
(α.vcomp β).app X = α.app X β.app X