Yoneda lemma related

Stream: mathlib4

[Luc Duponcheel]

Hello folks,

I'd like to contribute to mathlib4.
More precisely, in short, I have proved a specific Yoneda
lemma (for, what I call, Functional Categories), that I want
to make part of mathlib4.

So, naturally, I had a look at
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/CategoryTheory/Yoneda.lean.

The code contains an overwhelming amount of Yoneda-related theorems.

I may be wrong, but I did not find the theorem that I thought
was the Yoneda lemma I knew.

I saw coyonedaEquiv which is really cool!

But

1. coyonedaEquiv does not explicitly prove that
   fun _ x ↦ F.map x ξ is a natural transformation.
   Again, I may be wrong, maybe it somehow proves it implicitly.

2. coyonedaEquiv does not really deals with how
   both sides of the bijection relate to each other.

The code below deals with both 1. and 2. .

If the Mathlib experts know that the code is already dealt
with by the (overwhelming amount of) Yoneda-related theorems,
then, really, sorry for posting all this.

If not, then I would be more than willing to, somehow, add them to
mathlib4. Perhaps as a pull request?

Here is my code

Code listing

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic

import Mathlib.CategoryTheory.Functor.Hom

namespace CategoryTheory

open Opposite Category Functor

universe v₁ u₁

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

/-
This (slightly changed) definition is part of Mathlib.
-/

@[simps]
def coYoneda : Cᵒᵖ ⥤ (C ⥤ Type v₁) where
  obj Zop := let Z := unop Zop
    { obj := fun (Y : C) => Z ⟶ Y
      map := fun x2y => (· ≫ x2y) }
  map x2y := let y2x := x2y.unop
    { app := fun _ => (y2x ≫ ·) }

/-
This (slightly changed) definition is part of Mathlib.

It defines a bijection (via 'toFun' and 'invFun')

between

natural transformations
from 'coYoneda.obj (op Z)' (the coYoneda functor for Z)
to a preSheaf (a Type-valued functor)

and

values of Type 'preSheaf.obj Z'
-/
def coyonedaEquiv
    (Z : C)
    (preSheaf : C ⥤ Type v₁) :
  (coYoneda.obj (op Z) ⟶ preSheaf) ≃
    preSheaf.obj Z where
  toFun (natTransf : coYoneda.obj (op Z) ⟶ preSheaf) :=
    let preSheaf_Z : preSheaf.obj Z :=
      natTransf.app Z (𝟙 Z)
    preSheaf_Z
  invFun (preSheaf_Z : preSheaf.obj Z) :=
    let natTransf : coYoneda.obj (op Z) ⟶ preSheaf :=
      { app := fun Y z2y ↦ preSheaf.map z2y preSheaf_Z }
    natTransf
  left_inv := fun natTransf ↦ by
    ext Y (_ : Z ⟶ Y)
    dsimp
    rw [← FunctorToTypes.naturality]
    simp
  right_inv := by
    intro preSheaf_Z
    simp

/-
This theorem is not part of Mathlib.

It proves an equality
defining *how* a natural transformation
from 'coYoneda.obj (op Z)' (the coYoneda functor for Z)
to a preSheaf (a Type-valued functor)
can be defined in terms of a value of type 'preSheaf.obj Z'

The proof uses
'congr_fun (natTransf.naturality z2y) (𝟙 Z)'
-/
theorem coyoneda_1
    -- if given
    (Z : C)
    (preSheaf : C ⥤ Type v₁)
    (natTransf : coYoneda.obj (op Z) ⟶ preSheaf)
    -- then forall
    {Y : C}
    {z2y : Z ⟶ Y} :

  natTransf.app Y z2y
    = preSheaf.map z2y (natTransf.app Z (𝟙 Z)) :=

    let coYoneda_Z := coYoneda.obj (op Z)

    let preSheaf_Z := natTransf.app Z (𝟙 Z)

    calc

      natTransf.app Y z2y
        = natTransf.app Y (𝟙 Z ≫ z2y) := by
        simp -- z2y = 𝟙 Z ≫ z2y

    _   = (coYoneda_Z.map z2y ≫ natTransf.app Y) (𝟙 Z) :=
        rfl

    _   = (natTransf.app Z ≫ preSheaf.map z2y) (𝟙 Z) :=
        congr_fun -- F.map f ≫ app Y = app X ≫ G.map f
          (natTransf.naturality z2y) (𝟙 Z)

    _   = preSheaf.map z2y preSheaf_Z :=
        rfl

/-
This theorem proves that a transformation
defined in terms of a value of type 'preSheaf.obj Z'
(as in coyoneda_1 above)
is a natural transformation
(as in coyoneda_1 above)

-/
theorem coyoneda_2
    -- if given
    (Z : C)
    (preSheaf : C ⥤ Type v₁)
    (preSheaf_Z : preSheaf.obj Z)
    -- then forall
    {Y X : C}
    {y2x : Y ⟶ X}
    {z2y : Z ⟶ Y} :

  ((preSheaf.map · preSheaf_Z) ≫ preSheaf.map y2x) z2y
    = ((coYoneda.obj (op Z)).map y2x ≫
        (preSheaf.map · preSheaf_Z)) z2y :=

  let coYoneda_Z := coYoneda.obj (op Z)

  let transf_Z_Y : (Z ⟶ Y) → preSheaf.obj Y :=
    fun z2y ↦ preSheaf.map z2y preSheaf_Z

  let transf_Z_X : (Z ⟶ X) → preSheaf.obj X :=
    fun z2x ↦ preSheaf.map z2x preSheaf_Z

  calc
    (transf_Z_Y ≫ preSheaf.map y2x) z2y
     = (preSheaf.map y2x (preSheaf.map z2y preSheaf_Z)) :=
     rfl

  _  = (preSheaf.map (z2y ≫ y2x) preSheaf_Z) := by
    simp -- map (f ≫ g) = map f ≫ map g

  _  = (coYoneda_Z.map y2x ≫ transf_Z_X) z2y :=
     rfl

end CategoryTheory

[Lawrence Wu (llllvvuu)]

No need to apologize, the Zulip is the right place to ask given you already browsed the library. #Is there code for X? may be even better.

[Christian Merten]

The first two definitions exist in mathlib, as you note yourself.
Your coyoneda_1 can be proven by

  simp [← FunctorToTypes.naturality]

and your coyoneda_2 can be proven by

  simp

[Luc Duponcheel]

Christian Merten, thx, I'll give it a try.

Anyway, the general Yoneda Lemma was just a first try.
My main goal is to write my specific Yoneda Lemma (for Functional Categories) in Lean.

Thanks for the constructive answer. Much appreciated.

[Luc Duponcheel]

Christian Merten,

Thanks so much. You are my hero!

The code below, more in sync with the
Mathlib naming conventions, indeed, does the trick.

Impressive!

Frankly, with all those (co)yoneda theorems in
Mathlib/CategoryTheory/Yoneda.lean
it does not really come as a surprise
that my two theorems do not need a calc proof.

Do you think it is useful to add them to
Mathlib/CategoryTheory/Yoneda.lean
anyway (perhaps with a more approriate comment)?

Agreed, they deal with the how, while most other
ones deal with the what.

Code listing

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.Yoneda

namespace CategoryTheory

open Opposite Category Functor

universe v₁ u₁

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

/-
This theorem proves an equality
defining *how* a natural transformation
from 'coyoneda.obj (op Z)' (the coyoneda functor for Z)
to a presheaf (a Type-valued functor)
can be defined in terms of a value of type 'F.obj Z'
-/
theorem coyoneda_1
    -- if given
    (Z : C)
    (F : C ⥤ Type v₁)
    (η : coyoneda.obj (op Z) ⟶ F)
    -- then forall
    {Y : C}
    {z2y : Z ⟶ Y} :

  η.app Y z2y
    = F.map z2y (η.app Z (𝟙 Z)) :=
    by simp[← FunctorToTypes.naturality]

/-
This theorem proves that a transformation

defined in terms of a value of type 'F.obj Z'
as in coyoneda_1 above
is a natural transformation
-/
theorem coyoneda_2
    -- if given
    (Z : C)
    (F : C ⥤ Type v₁)
    (F_Z : F.obj Z)
    -- then forall
    {Y X : C}
    {y2x : Y ⟶ X}
    {z2y : Z ⟶ Y} :

  ((F.map · F_Z) ≫ F.map y2x) z2y
    = ((coyoneda.obj (op Z)).map y2x ≫
        (F.map · F_Z)) z2y := by simp

end CategoryTheory

The formulation and proof of my own specific
coyoneda will be another challenge ... .

I'll start with calc proofs and extract as many
intermediate lemmas as possible.

[Joël Riou]

If these lemmas appeared to be super useful in order to prove other significant things, they could be considered for inclusion, but so far, I do not think there is a need for the addition of these two lemmas.

[Luc Duponcheel]

Christian and Joël,

Greetings from the Lean workshop.

Thanks for your comments.

No my lemmas are not super useful in order to prove significant things that
cannot be proven by the existing ones.

However, the second one, slightly changed, (see code below) proves that invFun ξ satisfies the natural transformation law. As far as I understand, coyonedaEquiv, only deals with the "two-sided inverse" aspect.

But, then again, maybe some other theorem in the Yoneda.lean file already, explicitly or implicitly, proves that invFun ξ satisfies the natural transformation law.

Btw, I would have expected that I needed to help simp with Functor.map_comp, but it does not seem to be necessary.

Code listing

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.Yoneda

namespace CategoryTheory

open Opposite Category Functor

universe v₁ u₁

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

/-
def coyonedaEquiv {Z : C} {F : C ⥤ Type v₁} : (coyoneda.obj (op Z) ⟶ F) ≃ F.obj Z where
  toFun η := η.app Z (𝟙 Z)
  invFun ξ := { app := fun _ x ↦ F.map x ξ }
  left_inv := fun η ↦ by
    ext Y (_ : Z ⟶ Y)
    dsimp
    rw [← FunctorToTypes.naturality]
    simp
  right_inv := by intro ξ; simp
-/

theorem equivNaturality {Z Y X : C} {y2x : Y ⟶ X} {z2y : Z ⟶ Y} {F : C ⥤ Type v₁}
    (ξ : F.obj Z) :

  let invFun : F.obj Z → NatTrans (coyoneda.obj (op Z)) F :=
    fun ξ ↦ { app := fun _ x ↦ F.map x ξ }

  ((invFun ξ).app Y ≫ F.map y2x) z2y
    = ((coyoneda.obj (op Z)).map y2x ≫ (invFun ξ).app X) z2y := by
    simp

end CategoryTheory

[Joël Riou]

I do not know what you are trying to say, but in the definition of coyonedaEquiv, the line invFun ξ := { app := fun _ x ↦ F.map x ξ } construct a natural transformation: the code only gives the data of the app field, because the proof of the naturality field is filled automatically. There is no point stating this as a separate lemma.

[Luc Duponcheel]

Thanks so much Joël,

So do you mean that the fact the signature of my invFun definition mentions NaTransautomatically (not to say automagically) proves that the naturality law is satified? I was not aware of that specific power of Lean. I am relatively new.

[Joël Riou]

The naturality is part of the "axioms" that are satisfied by any object of type NatTrans F G. If one constructs something in NatTrans F G, then it must be a natural transformation.
In the category theory part of mathlib, many obvious and not so obvious commutativity of diagrams are proven automatically.

[Luc Duponcheel]

OK, poof by construction at type level. Cool.

[Chris Henson]

To answer the "automatically" question a bit more, in Lean you can in a typeclass definition specify a tactic that will be tried by default when not otherwise specified. Much of the category theory in Mathlib does this. To be specific in the above example, NatTrans is given some specified data app, and the naturality field is inferred by a tactic cat_disch that will call automation like aesop and simp.

[Luc Duponcheel]

Ok, I saw this cat_dish several times when browsing the source code, but I was not aware of its power. Thanks again Chris and Joël. I am still learning while trying, at the same time, to be creative as well. For my own specific Yoneda-like lemma for FunctionalCategory I can then, most probably, do similar things. Anyway, I will first start with a "low profile" calc based proof and then provide as much "high profile" features Ihat I understand. You are my heros.

[Luc Duponcheel]

Hello, folks,

I am a little bit ashamed to ask this question.

I thought I was becoming an experienced calc
based theorem prover, but now I am stuck with
(what I thought of as) two easy have's.

The MWE code below starts with minimal "low-profile"
Category and Functor stuff, and continues with my own
minimal PreFunctionalCategory.

I prove a theorem using the two have's
(they use sorry).

The first have corresponds to the definition of
toGlobal, so I would expect to be able to replace
sorry by rfl.

The second have uses the instance : Category function,
and I would also expect to be able to replace sorry
by rfl.

All comments are welcome.

Code listing

namespace Question

#eval "- begin -"

abbrev function t₀ t₁ := t₀ → t₁

abbrev unaryTypeConstructor := Type → Type

abbrev binaryTypeConstructor := Type → Type → Type

abbrev Global(btc : binaryTypeConstructor) := btc Unit

class Category (btc : binaryTypeConstructor) where

  ι {t : Type} : btc t t

  andThen {t₀ t₁ t₂ : Type} :
    btc t₀ t₁ → btc t₁ t₂ → btc t₀ t₂

export Category (ι andThen)

infixr:80 " ≫ " => andThen

instance :
  Category function := {

    ι {t : Type} :
      function t t :=
         id

    andThen {t₀ t₁ t₂ : Type} :
      function t₀ t₁ → function t₁ t₂ → function t₀ t₂ :=
        λ t₀2t₁ t₁2t₂ ↦ t₁2t₂ ∘ t₀2t₁
  }

class Functor
    (btc₀ : binaryTypeConstructor)
    (btc₁ : binaryTypeConstructor)
    (utc : unaryTypeConstructor) where

  φ {t₀ t₁ : Type} : btc₀ t₀ t₁ → btc₁ (utc t₀) (utc t₁)

export Functor (φ)

class FunctorLaws
    {btc₀ : binaryTypeConstructor}
    {btc₁ : binaryTypeConstructor}
    {utc : unaryTypeConstructor}
    [Category btc₀]
    [Category btc₁]
    (functor : Functor btc₀ btc₁ utc)
  : Prop where

  functor_sequential {t₀ t₁ t₂ : Type}
      {t₀2t₁ : btc₀ t₀ t₁}
      {t₁2t₂ : btc₀ t₁ t₂} :
    functor.φ t₀2t₁ ≫ functor.φ t₁2t₂
      = functor.φ (t₀2t₁ ≫ t₁2t₂)

export FunctorLaws (
  functor_sequential
)

class PreFunctionalCategory
    (btc : binaryTypeConstructor)
  extends Category btc where

  -- function as morphism
  F2BTC : Functor function btc Id

  -- value to global value
  toGlobal {t : Type} (vₜ : t) :
    btc Unit t :=
      F2BTC.φ (fun _ : Unit => vₜ)

export PreFunctionalCategory (F2BTC toGlobal)

@[simp] theorem pointfreeApplication
    {btc : binaryTypeConstructor}
    [PreFunctionalCategory btc]
    {preFunctionalCategory : PreFunctionalCategory btc}
    {functionCategory : Category function}
    [FunctorLaws preFunctionalCategory.F2BTC]
    {t₀ t₁ : Type}
    {t₀2t₁ : function t₀ t₁}
    {vₜ₀ : t₀} :

  (toGlobal vₜ₀ ≫ F2BTC.φ t₀2t₁ : Global btc t₁)
    = toGlobal (t₀2t₁ vₜ₀) :=

  have h {t : Type} {vₜ : t} :
    (toGlobal vₜ : btc Unit t)
      = F2BTC.φ (fun _ : Unit => vₜ)
      := sorry

  have h' {s t : Type} {vₛ : s} {s2t : function s t} :
    (fun _ : Unit => vₛ) ≫ s2t
      = fun _ : Unit => s2t vₛ
      := sorry

  calc
    (toGlobal vₜ₀ ≫ F2BTC.φ t₀2t₁ : Global btc t₁)
      = F2BTC.φ (fun _ : Unit => vₜ₀) ≫ F2BTC.φ t₀2t₁
      := congrArg (. ≫ F2BTC.φ t₀2t₁) h
  _   = F2BTC.φ ((fun _ : Unit => vₜ₀) ≫ t₀2t₁)
      := functor_sequential
  _   = F2BTC.φ (fun _ : Unit => t₀2t₁ vₜ₀)
      := congrArg (F2BTC.φ .) h'
  _   = toGlobal (t₀2t₁ vₜ₀)
      := Eq.symm h

#eval "-- end --"

end Question

[Luc Duponcheel]

FYI : I could solve the problem using two sub-optimal hacks. I'll post the code tomorrow. I'm gonna :sleeping: now