Yoneda lemma and category theory in Lean

Stream: new members

[Jonas van der Schaaf]

I've been trying to do category theory in Lean and need to use the Yoneda lemma to prove something "trivial" but I'm not sure how to do this. What I want to prove should be a corollary from the naturality of the Yoneda lemma, but there's too many variables and moving parts for my brain to parse this. See my code below:

import Mathlib

open CategoryTheory Opposite

universe u v

variable {C : Type u} [Category.{v} C] {X Y : C} (f : X ⟶ Y) {A : Cᵒᵖ ⥤ Type v} (g : yoneda.obj Y ⟶ A)

example : A.map (op f) (((yonedaLemma C).app ⟨op Y, A⟩).hom g).down = (((yonedaLemma C).app ⟨op X, A⟩).hom (yoneda.map f ≫ g)).down := by
  sorry

On another note: is there some general introduction to category theory in Lean? I've been trying to muddle my way through, but feel like I could use some reference material to learn things the "proper" way.

[Joël Riou]

It seems the lemma you are looking for is yonedaEquiv_naturality:

import Mathlib.CategoryTheory.Yoneda
open CategoryTheory Opposite
universe u v
variable {C : Type u} [Category.{v} C] {X Y : C} (f : X ⟶ Y)
  {A : Cᵒᵖ ⥤ Type v} (g : yoneda.obj Y ⟶ A)

example : A.map f.op (yonedaEquiv g) = yonedaEquiv (yoneda.map f ≫ g) :=
  yonedaEquiv_naturality g f

I would advise not to use yonedaLemma but rather yonedaEquiv, because the former needs the introduction of the uliftFunctor from one universe to a higher universe.