Natural transformations between functors between large categories

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-17.
Last modified on 2023-11-24.

module category-theory.natural-transformations-functors-large-categories where
Imports 
open import category-theory.functors-large-categories
open import category-theory.large-categories
open import category-theory.natural-transformations-functors-large-precategories

open import foundation.universe-levels

Idea

Given large categories C and D, a natural transformation from a functor F : C → D to G : C → D consists of :

  • a family of morphisms γ : (x : C) → hom (F x) (G x) such that the following naturality condition holds:
  • (G f) ∘ (γ x) = (γ y) ∘ (F f), for all f : hom x y.

Definition

module _
  {αC αD γF γG : Level → Level}
  {βC βD : Level → Level → Level}
  (C : Large-Category αC βC)
  (D : Large-Category αD βD)
  (F : functor-Large-Category γF C D)
  (G : functor-Large-Category γG C D)
  where

  family-of-morphisms-functor-Large-Category : UUω
  family-of-morphisms-functor-Large-Category =
    family-of-morphisms-functor-Large-Precategory
      ( large-precategory-Large-Category C)
      ( large-precategory-Large-Category D)
      ( F)
      ( G)

  naturality-family-of-morphisms-functor-Large-Category :
    family-of-morphisms-functor-Large-Category → UUω
  naturality-family-of-morphisms-functor-Large-Category =
    naturality-family-of-morphisms-functor-Large-Precategory
      ( large-precategory-Large-Category C)
      ( large-precategory-Large-Category D)
      ( F)
      ( G)

  natural-transformation-Large-Category : UUω
  natural-transformation-Large-Category =
    natural-transformation-Large-Precategory
      ( large-precategory-Large-Category C)
      ( large-precategory-Large-Category D)
      ( F)
      ( G)

  hom-natural-transformation-Large-Category :
    natural-transformation-Large-Category →
    family-of-morphisms-functor-Large-Category
  hom-natural-transformation-Large-Category =
    hom-natural-transformation-Large-Precategory

  naturality-natural-transformation-Large-Category :
    (τ : natural-transformation-Large-Category) →
    naturality-family-of-morphisms-functor-Large-Category
      (hom-natural-transformation-Large-Category τ)
  naturality-natural-transformation-Large-Category =
    naturality-natural-transformation-Large-Precategory

Properties

The identity natural transformation

Every functor comes equipped with an identity natural transformation.

module _
  { αC αD γF : Level → Level}
  { βC βD : Level → Level → Level}
  ( C : Large-Category αC βC)
  ( D : Large-Category αD βD)
  ( F : functor-Large-Category γF C D)
  where

  hom-id-natural-transformation-Large-Category :
    family-of-morphisms-functor-Large-Category C D F F
  hom-id-natural-transformation-Large-Category =
    hom-id-natural-transformation-Large-Precategory
      ( large-precategory-Large-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  naturality-id-natural-transformation-Large-Category :
    naturality-family-of-morphisms-functor-Large-Category C D F F
      hom-id-natural-transformation-Large-Category
  naturality-id-natural-transformation-Large-Category =
    naturality-id-natural-transformation-Large-Precategory
      ( large-precategory-Large-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  id-natural-transformation-Large-Category :
    natural-transformation-Large-Category C D F F
  id-natural-transformation-Large-Category =
    id-natural-transformation-Large-Precategory
      ( large-precategory-Large-Category C)
      ( large-precategory-Large-Category D)
      ( F)

Composition of natural transformations

module _
  {αC αD γF γG γH : Level → Level}
  {βC βD : Level → Level → Level}
  (C : Large-Category αC βC)
  (D : Large-Category αD βD)
  (F : functor-Large-Category γF C D)
  (G : functor-Large-Category γG C D)
  (H : functor-Large-Category γH C D)
  (τ : natural-transformation-Large-Category C D G H)
  (σ : natural-transformation-Large-Category C D F G)
  where

  hom-comp-natural-transformation-Large-Category :
    family-of-morphisms-functor-Large-Category C D F H
  hom-comp-natural-transformation-Large-Category =
    hom-comp-natural-transformation-Large-Precategory
      ( large-precategory-Large-Category C)
      ( large-precategory-Large-Category D)
      ( F)
      ( G)
      ( H)
      ( τ)
      ( σ)

  naturality-comp-natural-transformation-Large-Category :
    naturality-family-of-morphisms-functor-Large-Category C D F H
      hom-comp-natural-transformation-Large-Category
  naturality-comp-natural-transformation-Large-Category =
    naturality-comp-natural-transformation-Large-Precategory
      ( large-precategory-Large-Category C)
      ( large-precategory-Large-Category D)
      ( F)
      ( G)
      ( H)
      ( τ)
      ( σ)

  comp-natural-transformation-Large-Category :
    natural-transformation-Large-Category C D F H
  comp-natural-transformation-Large-Category =
    comp-natural-transformation-Large-Precategory
      ( large-precategory-Large-Category C)
      ( large-precategory-Large-Category D)
      ( F)
      ( G)
      ( H)
      ( τ)
      ( σ)

Recent changes