Mathlib.CategoryTheory.NatTrans

Module docstring

{"# 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.

CategoryTheory.NatTrans structure

(F G : C ⥤ D)

Full source

/-- `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`.
-/
@[ext]
structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where
  /-- The component of a natural transformation. -/
  app : ∀ X : C, F.obj X ⟶ G.obj X
  /-- The naturality square for a given morphism. -/
  naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f := by aesop_cat

Natural Transformation between Functors

Informal description

A natural transformation $\alpha : F \Rightarrow G$ between functors $F, G : \mathcal{C} \to \mathcal{D}$ consists of: - For each object $X$ in $\mathcal{C}$, a morphism $\alpha_X : F(X) \to G(X)$ (called the component of $\alpha$ at $X$) - For each morphism $f : X \to Y$ in $\mathcal{C}$, the naturality condition holds: $F(f) \circ \alpha_Y = \alpha_X \circ G(f)$ (expressed as a commutative square).

CategoryTheory.congr_app theorem

{F G : C ⥤ D} {α β : NatTrans F G} (h : α = β) (X : C) : α.app X = β.app X

Full source

theorem congr_app {F G : C ⥤ D} {α β : NatTrans F G} (h : α = β) (X : C) : α.app X = β.app X := by
  aesop_cat

Component Equality of Equal Natural Transformations

Informal description

For any two natural transformations $\alpha, \beta : F \Rightarrow G$ between functors $F, G : \mathcal{C} \to \mathcal{D}$, if $\alpha = \beta$, then their components at any object $X$ in $\mathcal{C}$ are equal, i.e., $\alpha_X = \beta_X$.

CategoryTheory.NatTrans.id definition

(F : C ⥤ D) : NatTrans F F

Full source

/-- `NatTrans.id F` is the identity natural transformation on a functor `F`. -/
protected def id (F : C ⥤ D) : NatTrans F F where app X := 𝟙 (F.obj X)

Identity natural transformation

Informal description

The identity natural transformation $\text{id}_F$ on a functor $F : \mathcal{C} \to \mathcal{D}$ is defined by assigning to each object $X$ in $\mathcal{C}$ the identity morphism $\text{id}_{F(X)} : F(X) \to F(X)$.

CategoryTheory.NatTrans.id_app' theorem

(F : C ⥤ D) (X : C) : (NatTrans.id F).app X = 𝟙 (F.obj X)

Full source

@[simp]
theorem id_app' (F : C ⥤ D) (X : C) : (NatTrans.id F).app X = 𝟙 (F.obj X) := rfl

Component of Identity Natural Transformation is Identity Morphism

Informal description

For any functor $F \colon \mathcal{C} \to \mathcal{D}$ and any object $X$ in $\mathcal{C}$, the component of the identity natural transformation $\mathrm{id}_F$ at $X$ is equal to the identity morphism $\mathrm{id}_{F(X)}$ on $F(X)$.

CategoryTheory.NatTrans.instInhabited instance

(F : C ⥤ D) : Inhabited (NatTrans F F)

Full source

instance (F : C ⥤ D) : Inhabited (NatTrans F F) := ⟨NatTrans.id F⟩

Inhabited Type of Endo-Natural Transformations

Informal description

For any functor $F : \mathcal{C} \to \mathcal{D}$, the type of natural transformations from $F$ to itself is inhabited by the identity natural transformation.

CategoryTheory.NatTrans.vcomp definition

(α : NatTrans F G) (β : NatTrans G H) : NatTrans F H

Full source

/-- `vcomp α β` is the vertical compositions of natural transformations. -/
def vcomp (α : NatTrans F G) (β : NatTrans G H) : NatTrans F H where
  app X := α.app X ≫ β.app X

-- functor_category will rewrite (vcomp α β) to (α ≫ β), so this is not a
-- suitable simp lemma.  We will declare the variant vcomp_app' there.

Vertical composition of natural transformations

Informal description

Given natural transformations $\alpha : F \Rightarrow G$ and $\beta : G \Rightarrow H$ between functors $F, G, H : \mathcal{C} \to \mathcal{D}$, their vertical composition $\alpha \circ \beta : F \Rightarrow H$ is defined by: - For each object $X$ in $\mathcal{C}$, the component $(\alpha \circ \beta)_X$ is the composition $\alpha_X \circ \beta_X$ in $\mathcal{D}$

CategoryTheory.NatTrans.vcomp_app theorem

(α : NatTrans F G) (β : NatTrans G H) (X : C) : (vcomp α β).app X = α.app X ≫ β.app X

Full source

theorem vcomp_app (α : NatTrans F G) (β : NatTrans G H) (X : C) :
    (vcomp α β).app X = α.app X ≫ β.app X := rfl

Component Formula for Vertical Composition of Natural Transformations

Informal description

For any natural transformations $\alpha : F \Rightarrow G$ and $\beta : G \Rightarrow H$ between functors $F, G, H : \mathcal{C} \to \mathcal{D}$, and for any object $X$ in $\mathcal{C}$, the component of the vertical composition $\alpha \circ \beta$ at $X$ is equal to the composition $\alpha_X \circ \beta_X$ in $\mathcal{D}$.