Natural transformations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[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₂)

app : Π (X : C), F.obj X ⟶ G.obj X
naturality' : (∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ self.app Y = self.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.

Instances for category_theory.nat_trans

category_theory.nat_trans.has_sizeof_inst
category_theory.nat_trans.inhabited

source

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

source

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

source

@[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

source

@[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'

source

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

source

@[protected]

def category_theory.nat_trans.id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

category_theory.nat_trans F F

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' := _}

source

@[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)

source

@[protected, instance]

def category_theory.nat_trans.inhabited {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

inhabited (category_theory.nat_trans F F)

Equations

category_theory.nat_trans.inhabited F = {default := category_theory.nat_trans.id F}

source

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} (α : category_theory.nat_trans F G) (β : category_theory.nat_trans G H) :

category_theory.nat_trans F H

vcomp α β is the vertical compositions of natural transformations.

Equations

α.vcomp β = {app := λ (X : C), α.app X ≫ β.app X, naturality' := _}

source

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