Documentation

Mathlib.CategoryTheory.NatTrans

Natural transformations #

Defines natural transformations between functors.

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

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

See also CategoryTheory.FunctorCat, where we provide the category structure on functors and natural transformations.

Introduces notations

source
ink
theorem CategoryTheory.NatTrans.ext {C : Type u₁} :
∀ {inst : CategoryTheory.Category C} {D : Type u₂} {inst_1 : CategoryTheory.Category D} {F G : C ⥤ D} (x y : CategoryTheory.NatTrans F G), x.app = y.app → x = y
source
ink
theorem CategoryTheory.NatTrans.ext_iff {C : Type u₁} :
∀ {inst : CategoryTheory.Category C} {D : Type u₂} {inst_1 : CategoryTheory.Category D} {F G : C ⥤ D} (x y : CategoryTheory.NatTrans F G), x = y ↔ x.app = y.app
source
ink
structure CategoryTheory.NatTrans {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) (G : C ⥤ D) :
Type (maxu₁v₂)

  • The component of a natural transformation.

    app : (X : C) → F.obj X ⟶ G.obj X

  • The naturality square for a given morphism.

    naturality : autoParam (∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f) _auto✝

NatTrans 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.

Instances For
    source
    ink
    def CategoryTheory.unexpandNatTransApp :
    Lean.PrettyPrinter.Unexpander

    This unexpander will pretty print η.app X properly. Without this, we would have NatTrans.app η X.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    ink
    @[simp]
    theorem CategoryTheory.NatTrans.naturality_assoc {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C ⥤ D} {G : C ⥤ D} (self : CategoryTheory.NatTrans F G) ⦃X : C⦄ ⦃Y : C⦄ (f : X ⟶ Y) {Z : D} (h : G.obj Y ⟶ Z) :
    F.map f ≫ self.app Y ≫ h = self.app X ≫ G.map f ≫ h
    source
    ink
    theorem CategoryTheory.congr_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C ⥤ D} {G : C ⥤ D} {α : CategoryTheory.NatTrans F G} {β : CategoryTheory.NatTrans F G} (h : α = β) (X : C) :
    α.app X = β.app X
    source
    ink
    def CategoryTheory.NatTrans.id {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) :
    CategoryTheory.NatTrans F F

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

    Equations
    source
    ink
    @[simp]
    theorem CategoryTheory.NatTrans.id_app' {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) (X : C) :
    (CategoryTheory.NatTrans.id F).app X = 𝟙 (F.obj X)
    source
    ink
    instance CategoryTheory.NatTrans.instInhabitedNatTrans {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C ⥤ D) :
    Inhabited (CategoryTheory.NatTrans F F)
    Equations
    source
    ink
    def CategoryTheory.NatTrans.vcomp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C ⥤ D} {G : C ⥤ D} {H : C ⥤ D} (α : CategoryTheory.NatTrans F G) (β : CategoryTheory.NatTrans G H) :
    CategoryTheory.NatTrans F H

    vcomp α β is the vertical compositions of natural transformations.

    Equations
    source
    ink
    theorem CategoryTheory.NatTrans.vcomp_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C ⥤ D} {G : C ⥤ D} {H : C ⥤ D} (α : CategoryTheory.NatTrans F G) (β : CategoryTheory.NatTrans G H) (X : C) :
    (CategoryTheory.NatTrans.vcomp α β).app X = α.app X ≫ β.app X