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

• τ.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 CategoryTheory.FunctorCat),
• σ ≫ τ for vertical compositions, and
• σ ◫ τ for horizontal compositions.

theorem CategoryTheory.NatTrans.ext_iff {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 = y ↔ x.app = y.app

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.app → x = y

structure CategoryTheory.NatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C D) : Type (max u₁ v₂)

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.

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

  The component of a natural transformation.

• naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (self.app Y) = CategoryTheory.CategoryStruct.comp (self.app X) (G.map f)

  The naturality square for a given morphism.

@[simp]

theorem CategoryTheory.NatTrans.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans F G) ⦃X : C⦄ ⦃Y : C⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (F.map f) (self.app Y) = CategoryTheory.CategoryStruct.comp (self.app X) (G.map f)

The naturality square for a given morphism.

@[simp]

theorem CategoryTheory.NatTrans.naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans F G) ⦃X : C⦄ ⦃Y : C⦄ (f : X ⟶ Y) {Z : D} (h : G.obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (self.app Y) h) = CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (G.map f) h)

theorem CategoryTheory.congr_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {α : CategoryTheory.NatTrans F G} {β : CategoryTheory.NatTrans F G} (h : α = β) (X : C) : α.app X = β.app X

def CategoryTheory.NatTrans.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.NatTrans F F

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

Equations

• CategoryTheory.NatTrans.id F = { app := fun (X : C) => CategoryTheory.CategoryStruct.id (F.obj X), naturality := ⋯ }

@[simp]

theorem CategoryTheory.NatTrans.id_app' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : (CategoryTheory.NatTrans.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)

instance CategoryTheory.NatTrans.instInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Inhabited (CategoryTheory.NatTrans F F)

Equations

• CategoryTheory.NatTrans.instInhabited F = { default := CategoryTheory.NatTrans.id F }

def CategoryTheory.NatTrans.vcomp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : CategoryTheory.NatTrans F G) (β : CategoryTheory.NatTrans G H) : CategoryTheory.NatTrans F H

vcomp α β is the vertical compositions of natural transformations.

Equations

• α.vcomp β = { app := fun (X : C) => CategoryTheory.CategoryStruct.comp (α.app X) (β.app X), naturality := ⋯ }

theorem CategoryTheory.NatTrans.vcomp_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : CategoryTheory.NatTrans F G) (β : CategoryTheory.NatTrans G H) (X : C) : (α.vcomp β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)