mathlib documentation

category_theory.natural_transformation

@[ext]
structure category_theory.nat_trans {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] :
C DC DType (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) :
x.app = y.appx = 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

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

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