post- and pre-composition natural transformations

Stream: general

[Chris Henson]

I'm trying to formalize a couple of the examples/exercises from Category Theory in Context. She defines:

image.png

and an example of these in natural transformations:

image.png

Here is how I wrote these:

import Mathlib

open CategoryTheory

universe u v

variable {C : Type u} [Category.{v} C]

-- definition 1.3.11
def postcomp (c : C) : C ⥤ Type v where
  obj (x : C) := c ⟶  x
  map {x y} (f : x ⟶  y) := (· ≫ f)

def precomp (c : C) : Cᵒᵖ ⥤ Type v where
  obj (x : Cᵒᵖ) := x.unop ⟶  c
  map {x y} (f : x ⟶  y) := (f.unop ≫ ·)

-- example 1.4.7
def postcomp_trans {w x: C} (f : w ⟶  x) : NatTrans (postcomp x) (postcomp w) where
  app (c : C) := precomp c |>.map f.op
  naturality:= by
    simp [postcomp, precomp]
    intros
    ext
    simp

def precomp_trans {y z: C} (h : y ⟶  z) : NatTrans (precomp y) (precomp z) where
  app (c : Cᵒᵖ) := postcomp c.unop |>.map h
  naturality := by
    simp [postcomp, precomp]
    intros
    ext
    simp

I understand that being representable is more general, but I wanted to replicate the example as is. The functor definitions seem fine, though I would appreciate confirmation I did the opposite category parts correct. What confused me was the natural transformations. Does what I wrote correspond to her examples correctly?

[Kim Morrison]

Did you have a question?

[Chris Henson]

Kim Morrison said:

Did you have a question?

My question was the last sentence "Does what I wrote correspond to her examples correctly?". It typechecked, but I was afraid I accidentally proved the wrong thing.

[Kim Morrison]

(Oh, sorry, I was confused by the image and missed the "below the fold"...)

[Kim Morrison]

Yes, these look good!

[Kim Morrison]

check out
docs#CategoryTheory.yoneda

[Kim Morrison]

It manages to do everything at once by defining a bifunctor:

def yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁ where
  obj X :=
    { obj := fun Y => unop Y ⟶ X
      map := fun f g => f.unop ≫ g }
  map f :=
    { app := fun _ g => g ≫ f }

It's fun to work out that this contains both precomp and precomp_trans.

[Kim Morrison]

And also fun to work out why we can omit all the proofs! :-)

[Chris Henson]

Okay thanks!

[Chris Henson]

Kim Morrison said:

And also fun to work out why we can omit all the proofs! :-)

Yes, the aesop_cat proofs are nice.