2-Yoneda Lemma

In mathematics, especially category theory, the 2-Yoneda lemma is a generalization of the Yoneda lemma to 2-categories. Precisely, given a contravariant pseudofunctor $F$ on a category ''C'', it says: for each object $x$ in ''C'', the natural functor (evaluation at the identity)
:$\underline(h_x, F) \to F(x)$
is an equivalence of categories, where $\underline(-, -)$ denotes (roughly) the category of natural transformations between pseudofunctors on ''C'' and $h_x = \operatorname(-, x)$.

Under the Grothendieck construction, $h_x$ corresponds to the comma category $C \downarrow x$. So, the lemma is also frequently stated as:
:$F(x) \simeq \underline(C \downarrow x, F),$
where $F$ is identified with the fibered category associated to $F$.

As an application of this lemma, the coherence theorem for bicategories holds.

Sketch of proof

First we define the functor in the opposite direction
:$\mu : F(x) \to \underline(h_x, F)$
as follows. Given an object $\overline$ in $F(x)$, define the natural transformation
:$\mu(\overline) : h_x \to F,$
that is, $\mu(\overline)_y : \operatorname(y, x) \to F(y),$ by
:$\mu(\overline)_y(f) = (Ff) \overline.$
(In the below, we shall often drop a subscript for a natural transformation.) Next, given a morphism $\varphi : \overline \to x'$ in $F(x)$, for $f : y \to x$, we let $\mu(\varphi)(f)$ be
:$(Ff)\varphi : (Ff)\overline \to (Ff)x'.$
Then $\mu(\varphi) :\mu(\overline) \to \mu(x')$ is a morphism (a 2-morphism to be precise or a modification in the terminology of Bénabou). The rest of the proof is then to show
# The above $\mu$ is a functor,
# $e \circ \mu \simeq \operatorname$, where $e$ is the evaluation at the identity; i.e., $e(\lambda) = \lambda(\operatorname_x),$ $e(\alpha : \lambda \to \rho) = \alpha(\operatorname_x) : \lambda(\operatorname_x) \to \rho(\operatorname_x),$
# $\mu \circ e \simeq \operatorname.$
Claim 1 is clear. As for Claim 2,
:$e(\mu(\overline)) = \mu(\overline)(\operatorname_x) = F(\operatorname_x) \overline \simeq \operatorname_ \overline = \overline$
where the isomorphism here comes from the fact that $F$ is a pseudofunctor. Similarly,$e(\mu(\varphi)) \simeq \varphi.$
For Claim 3, we have:
:$\mu(e(\lambda))(f) = (Ff \circ \lambda)(\operatorname_x) \simeq (\lambda \circ h_x f)(\operatorname_x) = \lambda(f).$
Similarly for a morphism $\alpha : \lambda \to \rho.$ $\square$

∞-Yoneda

Given an ∞-category ''C'', let $\widehat = \underline(C^, \textbf)$ be the ∞-category of presheaves on it with values in Kan = the ∞-category of Kan complexes. Then the ∞-version of the Yoneda embedding $C \hookrightarrow \widehat$ involves some (harmless) choice in the following way.

First, we have the hom-functor
:$\operatorname : C^ \times C \to \textbf$
that is characterized by a certain universal property (e.g., universal left fibration) and is unique up to a unique isomorphism in the homotopy category $\operatorname\underline(C \times C^, \textbf).$ Fix one such functor. Then we get the Yoneda embedding functor in the usual way:
:$y : C \to \widehat, \, a \mapsto \operatorname(-, a),$
which turns out to be fully faithful (i.e., an equivalence on the Hom level). Moreover and more strongly, for each object $F$ in $\widehat$ and object $a$ in $C$, the evaluation $e$ at the identity (see below)
:$\operatorname(y(a), F) \to F(a)$
is invertible in the ∞-category of large Kan complexes (i.e., Kan complexes living in a universe larger than the given one). Here, the evaluation map $e$ refers to the composition
:$\operatorname(y(a), F) \overset\to \operatorname(y(a)(a), F(a)) = \operatorname(\operatorname(a, a), F(a)) \to F(a)$
where the last map is the restriction to the identity $\operatorname_a$.

The ∞-Yoneda lemma is closely related to the matter of straightening and unstraightening.

Notes

References

*
*
*

Further reading

*
*
*
*
*
* E. Riehl and D. Verity, Fibrations and Yoneda’s lemma in an ∞-cosmos, J. Pure Appl. Algebra 221 (2017), no. 3, 499–564, arXiv:1506.05500
* https://math.stackexchange.com/questions/1293920/yoneda-lemma-for-2-categories-lax-version
*
*
*
*{{Cite web , title=2.2 The Theory of 2-Categories , url=https://kerodon.net/tag/007K , website=Kerodon, ref={{harvid, 8.3.3 Hom-Functors for ∞-Categories in Kerodon
Category theory