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, and the naturality squares α.naturality f : F.map f ≫ α.app Y = α.app X ≫ G.map f, where f : X ⟶ 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

theorem CategoryTheory.NatTrans.ext {C : Type u₁} :
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {F G : CategoryTheory.Functor C D} (x y : CategoryTheory.NatTrans F G), x.app = y.appx = y

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

    The naturality square for a given morphism.

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

    Equations
    Instances For

      vcomp α β is the vertical compositions of natural transformations.

      Equations
      Instances For