Yoneda lemma proves that nattrans is a set

Stream: new members

[Shanghe Chen]

Hi I am trying to understand the implementation of the Yoneda in lean with https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Yoneda.html#CategoryTheory.yonedaLemma . And Emily Riehl says in /Category Theory in context/ that:

[Shanghe Chen]

““As C is locally small but not necessarily small, a priori the collection of natural transformations Hom(C(c, −), F) might be large. However, the bijection in the Yoneda lemma proves that this particular collection of natural transformations indeed forms a set.”

[Shanghe Chen]

Is this some kind also proved in the above implementation? It seems like about lowering the universe level by one. Or is it possible to state with current universe arithmetic?

[Joël Riou]

The bijection is docs#CategoryTheory.yonedaEquiv, then this particular set of natural transformations is in bijection with F.obj (Opposite.op X). In Lean/mathlib, each category C has two attached universes: the universe u such that C : Type u and the universe v such that (X ⟶ Y) : Type v for all X and Y. Then, a priori, the type of natural transformations is in Type (max u v), but the bijection in Yoneda's lemma shows it is in bijection with a type in Type v.

In the case of a "large category", u = v + 1, so that this indeed lowers the universe level by one.

[Shanghe Chen]

Thank you very much Joël. Just found that https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Equiv/Defs.html#Equiv can be used for two types of different universes. Yeah then yonedaEquiv is exactly what Riehl means I think :tada: