Coyoneda Lemma

Stream: Is there code for X?

[Christian Merten]

Is there a convenient way to obtain the following coyoneda lemma?

import Mathlib

universe u v

open CategoryTheory Limits

variable {C : Type u} [Category.{v} C] (F : C ⥤ Type v)

def coyonedaSections (X : Cᵒᵖ) :
    (coyoneda.obj X ⟶ F) ≅ uliftFunctor.{u, v}.obj (F.obj X.unop) := sorry

There is docs#CategoryTheory.yonedaSections, and by some arrow reversing this version should be obtainable from that. But since Cᵒᵖᵒᵖ is not def-eq to C, this gets a bit messy.

[Adam Topaz]

can you use docs#CategoryTheory.unopUnop or docs#CategoryTheory.opOp ?

[Christian Merten]

I tried, but that's what I meant by it gets messy:

import Mathlib

universe u v

open CategoryTheory Limits

section

variable {C D E : Type*} [Category C] [Category D] [Category E] (H : C ≌ D) (F G : D ⥤ E)

def help0 : (F ⟶ G) ≃ (H.functor ⋙ F ⟶ H.functor ⋙ G) := sorry

end

section

variable {C : Type u} [Category.{v} C] (F : C ⥤ Type v)

def help1 (X : Cᵒᵖ) : (coyoneda.obj X ⟶ F) ≃ (unopUnop C ⋙ coyoneda.obj X ⟶ unopUnop C ⋙ F) :=
  help0 (opOpEquivalence C) (coyoneda.obj X) F

def aux' (X : Cᵒᵖ) : (yoneda.obj X ⟶ unopUnop C ⋙ F) ≃ (coyoneda.obj X ⟶ F) := by
  trans
  · show (yoneda.obj X ⟶ unopUnop C ⋙ F) ≃ (unopUnop C ⋙ coyoneda.obj X ⟶ unopUnop C ⋙ F)
    admit
  · exact (help1 F X).symm

def coyonedaLemma (X : Cᵒᵖ) :
    (coyoneda.obj X ⟶ F) ≅ uliftFunctor.{u, v}.obj (F.obj X.unop) := by
  trans
  · exact Iso.symm <| Equiv.toIso <| aux' F X
  · exact yonedaSections X (unopUnop C ⋙ F)

end

I also tried to construct aux' by hand, which also gets annoying very fast.

[Adam Topaz]

bah, at this point maybe you should just do it by hand!

import Mathlib

universe u v

open CategoryTheory Limits

variable {C : Type u} [Category.{v} C] (F : C ⥤ Type v)

def coyonedaSections (X : Cᵒᵖ) : (coyoneda.obj X ⟶ F) ≅ uliftFunctor.{u, v}.obj (F.obj X.unop) where
  hom η := .up <| η.app _ <| 𝟙 _
  inv ξ := { app := fun Y x => F.map x ξ.down }
  hom_inv_id := by
    ext η Y t
    simpa using (congr_fun (η.naturality t) (𝟙 _)).symm

[Christian Merten]

Thank you! Should we just copy the respective section in CategoryTheory.Yoneda and dualize all results?

[Adam Topaz]

Probably yeah

[Christian Merten]

I wish someday there is a @[reverse_arrows].

[Christian Merten]

I did that in #12041.

[Robert Maxton]

I was just looking for that ^.^;