Library HoTT.categories.NaturalTransformation.Core

Definition of natural transformation

Require Import Category.Core Functor.Core.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Delimit Scope natural_transformation_scope with natural_transformation.

Local Open Scope morphism_scope.
Local Open Scope natural_transformation_scope.

Section NaturalTransformation.
  Variables C D : PreCategory.
  Variables F G : Functor C D.

Quoting from the lecture notes for 18.705, Commutative Algebra:
A map of functors is known as a natural transformation. Namely, given two functors F : C D, G : C D, a natural transformation T: F G is a collection of maps T A : F A G A, one for each object A of C, such that (T B) (F m) = (G m) (T A) for every map m : A B of C; that is, the following diagram is commutative:
           F m
     F A -------> F B
      |            |
      |            |
      | T A        | T B
      |            |
      V    G m     V
     G A --------> G B

  Record NaturalTransformation :=
    Build_NaturalTransformation' {
        components_of :> c, morphism D (F c) (G c);
        commutes : s d (m : morphism C s d),
                     components_of d o F _1 m = G _1 m o components_of s;
        
        commutes_sym : s d (m : C.(morphism) s d),
                         G _1 m o components_of s = components_of d o F _1 m
      }.

  Definition Build_NaturalTransformation CO COM
    := Build_NaturalTransformation'
         CO
         COM
         (fun _ _ _symmetry _ _ (COM _ _ _)).
End NaturalTransformation.

Bind Scope natural_transformation_scope with NaturalTransformation.

Create HintDb natural_transformation discriminated.

Global Arguments components_of {C D}%category {F G}%functor T%natural_transformation /
          c%object : rename.
Global Arguments commutes {C D F G} !T / _ _ _ : rename.
Global Arguments commutes_sym {C D F G} !T / _ _ _ : rename.

Hint Resolve @commutes : category natural_transformation.

Helper lemmas

Some helper lemmas for rewriting. In the names, p stands for a morphism, T for natural transformation, and F for functor.
Definition commutes_pT_F C D (F G : Functor C D) (T : NaturalTransformation F G)
      s d d' (m : morphism C s d) (m' : morphism D _ d')
: (m' o T d) o F _1 m = (m' o G _1 m) o T s
  := ((Category.Core.associativity _ _ _ _ _ _ _ _)
        @ ap _ (commutes _ _ _ _)
        @ (Category.Core.associativity_sym _ _ _ _ _ _ _ _))%path.

Definition commutes_T_Fp C D (F G : Functor C D) (T : NaturalTransformation F G)
      s d d' (m : morphism C s d) (m' : morphism D d' _)
: T d o (F _1 m o m') = G _1 m o (T s o m')
  := ((Category.Core.associativity_sym _ _ _ _ _ _ _ _)
        @ ap10 (ap _ (commutes _ _ _ _)) _
        @ (Category.Core.associativity _ _ _ _ _ _ _ _))%path.