nLab
Yoneda lemma for bicategories

Context

Yoneda lemma

2-category theory

Contents

Statement

The Yoneda lemma for bicategories is a version of the Yoneda lemma that applies to bicategories, the most common algebraic sort of weak 2-category. It says that for any bicategory CC, any object xCx\in C, and any pseudofunctor F:C opCatF\colon C^{op}\to Cat, there is an equivalence of categories

[C op,Cat](C(,x),F)F(x) [C^{op},Cat](C(-,x), F) \simeq F(x)

which is pseudonatural in xx and FF, and which is given by evaluation at 1 x1_x, i.e. α:C(,x)F\alpha\colon C(-,x)\to F maps to α x(1 x)\alpha_x(1_x).

For bicategories AA and BB, [A,B][A,B] denotes the bicategory of pseudofunctors, pseudonatural transformations, and modifications from AA to BB. Note that it is a strict 2-category as soon as BB is.

Implications

In particular, the Yoneda lemma for bicategories implies that there is a Yoneda embedding for bicategories C[C op,Cat]C\to [C^{op},Cat] which is 2-fully-faithful?, i.e. an equivalence on hom-categories. Therefore, CC is equivalent to a sub-bicategory of [C op,Cat][C^{op},Cat]. Since Cat is a strict 2-category, it follows that CC is equivalent to a strict 2-category, which is one form of the coherence theorem for bicategories. (Conversely, another form of the coherence theorem can be used to prove the Yoneda lemma; see below.)

Proof

A detailed proof of the bicategorical Yoneda lemma seems to be hard to find in the literature. (Anyone have references to add?)

Explicit proof

An explicit proof, involving many diagrams, has been written up by Igor Baković and can be found here.

High-technology proof

We will take it for granted that [C op,Cat][C^{op},Cat] is a well-defined bicategory; this is a basic fact having nothing to do with the Yoneda lemma. We also take it as given that “evaluation at 1 x1_x” functor

[C op,Cat](C(,x),F)F(x) [C^{op},Cat](C(-,x), F) \to F(x)

is well-defined and pseudonatural in FF and xx; our goal is to prove that it is an equivalence. (Granted, these basic facts require a fair amount of verification as well.)

We will use part of the coherence theorem for pseudoalegbras?, which says that for a suitably well-behaved strict 2-monad TT, the inclusion TT-Alg strictPsAlg_{strict} \hookrightarrow Ps-TT-AlgAlg of the 2-category of strict TT-algebras and strict TT-morphisms into the 2-category of pseudo TT-algebras and pseudo TT-morphisms has a left adjoint, usually written as ()(-)'. Moreover, for any pseudo TT-algebra AA, the unit AAA\to A' is an equivalence in PsPs-TT-AlgAlg.

First, there is a 2-monad TT such that strict TT-algebras are strict 2-categories, strict TT-morphisms are strict 2-functors, pseudo TT-algebras are unbiased bicategories?, and pseudo TT-morphisms are pseudofunctors. By Mac Lane’s coherence theorem for bicategories, any ordinary bicategory can equally well be considered as an unbiased one. Thus, since CatCat is a strict 2-category, for any bicategory CC there is a strict 2-category CC' such that pseudofunctors CCatC\to Cat are in bijection with strict 2-functors CCatC'\to Cat.

Now note that a pseudonatural transformation between two pseudofunctors (resp. strict 2-functors) CDC\to D is the same as a single pseudofunctor (resp. strict 2-functor) CCyl(D)C\to Cyl(D), where Cyl(D)Cyl(D) is the bicategory whose objects are the 1-cells of DD, whose 1-cells are squares in DD commuting up to isomorphism, and whose 2-cells are “cylinders” in DD. Likewise, a modification between two such transformations is the same as a single functor (of whichever sort) C2Cyl(D)C\to 2Cyl(D), where the objects of 2Cyl(D)2Cyl(D) are the 2-cells of DD, and so on. Therefore, CC' classifies not only pseudofunctors out of CC, but transformations and modifications between them; thus we have an isomorphism

[C op,Cat][(C) op,Cat] strict,pseudo[C^{op},Cat] \cong [(C')^{op},Cat]_{strict,pseudo}

where [A,B] strict,pseudo[A,B]_{strict,pseudo} denotes the 2-category of strict 2-functors, pseudonatural transformations, and modifications between two strict 2-categories. Thus we can equally well analyze the functor

[(C) op,Cat] strict,pseudo(C(,x)¯,F¯)F¯(x)=F(x) [(C')^{op},Cat]_{strict,pseudo}(\overline{C(-,x)}, \overline{F}) \to \overline{F}(x) = F(x)

given by evaluation at 1 x1_x. Here C(,x)¯\overline{C(-,x)} and F¯\overline{F} denote the strict 2-functors (C) opCat(C')^{op}\to Cat corresponding to the pseudofunctors C(,x)C(-,x) and FF under the ()(-)' adjunction. However, we also have a strict 2-functor C(,x)C'(-,x), and the equivalence CCC\simeq C' induces an equivalence C(,x)C(,x)¯C'(-,x)\simeq \overline{C(-,x)}. Therefore, it suffices to analyze the functor

[(C) op,Cat] strict,pseudo(C(,x),F¯)F¯(x). [(C')^{op},Cat]_{strict,pseudo}(C'(-,x), \overline{F}) \to \overline{F}(x).

Now for any AA and BB, we have an inclusion functor [A,B] strict,strict[A,B] strict,pseudo[A,B]_{strict,strict} \to [A,B]_{strict,pseudo} where [A,B] strict,strict[A,B]_{strict,strict} denotes the 2-category of strict 2-functors, strict 2-natural transformations, and modifications. This functor is bijective on objects and locally fully faithful. Moreover, the composite

[(C) op,Cat] strict,strict(C(,x),F¯)[(C) op,Cat] strict,pseudo(C(,x),F¯)F¯(x). [(C')^{op},Cat]_{strict,strict}(C'(-,x), \overline{F}) \to [(C')^{op},Cat]_{strict,pseudo}(C'(-,x), \overline{F}) \to \overline{F}(x).

is an isomorphism, by the Yoneda lemma for enriched categories?, in the special case of CatCat-enrichment. Since

[(C) op,Cat] strict,strict(C(,x),F¯)[(C) op,Cat] strict,pseudo(C(,x),F¯)[(C')^{op},Cat]_{strict,strict}(C'(-,x), \overline{F}) \to [(C')^{op},Cat]_{strict,pseudo}(C'(-,x), \overline{F})

is fully faithful, if we can show that it is essentially surjective, then the 2-out-of-3 property for equivalences of categories will imply that the desired functor is an equivalence.

Here we at last descend to something concrete. Given α:C(,x)F¯\alpha\colon C'(-,x)\to \overline{F}, we have an obvious choice for a strict transformation for it to be equivalent to, namely β\beta whose components β y:C(y,x)F¯(y)\beta_y\colon C'(y,x)\to \overline{F}(y) is given by fF¯(f)(a)f \mapsto \overline{F}(f)(a) where a=α x(1 x)F¯(x)a = \alpha_x(1_x)\in \overline{F}(x). Since α\alpha is pseudonatural, for any f:yxf\colon y\to x in CC' we have an isomorphism

α y(f)=α y(f1 x)F¯(f)(α x(1 x))=F¯(f)(a)=β y(f).\alpha_y(f) = \alpha_y(f\circ 1_x) \cong \overline{F}(f)(\alpha_x(1_x)) = \overline{F}(f)(a) = \beta_y(f).

We then simply verify that these isomorphisms are the components of an (invertible) modification αβ\alpha\cong \beta. This completes the proof.

Revised on October 22, 2013 19:58:01 by David Roberts (129.127.252.5)