Finn Lawler free 2-cocompletion (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

We want to show that if KK is a bicategory then PK=[K op,Cat]P K = [K^{op}, Cat] is the free 2-cocompletion of KK.

There are several kinds of 2-colimit that we’ll need to talk about. Let D:JKD \colon J \to K and W:J opCatW \colon J^{op} \to Cat be pseudofunctors. Then

  1. The 2-colimit WDW \star D satisfies

    K(WD,X)[J op,Cat](W,K(D,X)) K(W \star D, X) \simeq [J^{op}, Cat](W, K(D-, X))

    This is what in the literature is often called a bilimit.

  2. If KK is a strict 2-category, the pseudocolimit W pDW \star_{p} D satisfies the same property up to isomorphism.

  3. If KK is strict and WW and DD are strict 2-functors, then the strict pseudocolimit W p sDW \star^s_{p} D satisfies

    K(W p sD,X)Ps(J op,Cat)(W,K(D,X)) K(W \star^s_p D, X) \cong Ps(J^{op}, Cat)(W, K(D-, X))

    where on the right the functor category is that of strict 2-functors, pseudonatural transformations and modifications.

  4. Under the same hypotheses, the strict colimit W s sDW \star^s_s D satisfies

    K(W s sD,X)Str(J op,Cat)(W,K(D,X)) K(W \star^s_s D, X) \cong Str(J^{op}, Cat)(W, K(D-, X))

    where now StrStr denotes the category of strict 2-functors and strict transformations (and modifications).

We need to show that PKP K has all small 2-colimits:

  1. CatCat is strictly 2-cocomplete: its underlying 1-category has small colimits, and CatCat is enriched and tensored over itself, so that it has strict CatCat-weighted colimits.

  2. Pseudocolimits, strict or otherwise, are a fortiori 2-colimits, and strict pseudocolimits are just strict colimits whose weights are ‘cofibrant’ in a suitable sense. Moreover, if KK is a strict 2-category, then for any index bicategory JJ there is a strict 2-category JJ' such that strict functors JKJ' \to K are the same thing as pseudofunctors JKJ \to K, and the 2-colimit of pseudofunctors WDW \star D is equivalent to the strict pseudocolimit of the strictified functors. So a strictly 2-cocomplete strict 2-category is also 2-cocomplete.

  3. PK=[K op,Cat] P Cat K = [K^{op}, Cat] is therefore a strict 2-category, and it has all non-strict strict 2-colimits. ( We can now try to compute colimits pointwise in Cat PK Cat P K -weighted) colimits, which are computed pointwise as usual for enriched strictly-enriched functor categories: if nowD:JPKD \colon J \to P K and W:J opCatW \colon J^{op} \to Cat are strict, then we set can define(W s sD)a=W s sD(,a) (W \star^s_s \star D) a = W \star^s_s \star D(-,a) , and verify its universal property: property follows:

    PK(W s sD,F) aCat(W s sD(,a),Fa) aStr[(J op,Cat ) ](W,Cat(D(,a),Fa)) Str[(J op,Cat ) ](W,P a K Cat(D (,a),Fa)) [J op,Cat](W,PK(D,F)) \array{ P K(W \star^s_s \star D, F) & \simeq \int_a Cat(W \star^s_s \star D(-,a), F a) \\ & \simeq \int_a Str(J^{op}, [J^{op}, Cat)(W, Cat](W, Cat(D(-,a), F a)) \\ & \simeq Str(J^{op}, [J^{op}, Cat)(W, Cat](W, \int_a Cat(D(-,a), F a)) \\ & \simeq [J^{op}, Cat](W, P K(D-, F)) }

    So PKP K has 2-colimits.

So Finally, we need to show that if P LK P L K has is strict a 2-colimits cocomplete and bicategory, hence then also there non-strict is 2-colimits. a 2-equivalence

Finally, we need to show that if LL is a cocomplete bicategory, then there is a 2-equivalence

Cocont(PK,L)[K,L] Cocont(P K, L) \sim [K, L]
Cocont(PK,L)[K,L] Cocont(P K, L) \sim [K, L]

For this we simply follow the usual reasoning: from left to right we compose with the Yoneda embedding y:KPKy \colon K \to P K, and given a functor F:KLF \colon K \to L we get a cocontinuous PKLP K \to L sending W:K opCatW \colon K^{op} \to Cat to WFW \star F.

For The this co-Yoneda we lemma simply shows follow that the every usual reasoning: from left to right we compose with the Yoneda embeddingWWy:KPK W \simeq W \star y \colon K \to P K , and given if a functor F H:KL F H \colon K \to L we is get a cocontinuous then P HK(WL)H(Wy)WHy P H(W) K \simeq \to H(W L \star y) \simeq W \star H y , sending showing that the functor W F :K op Cat F W F \colon \mapsto K^{op} - \to \star Cat F to is essentially surjective. It is 2-fully-faithful by the universal property of colimits: a transformationWFG W \star F \to G gives rise to an essentially unique transformation FG-\star F \to -\star G.

The co-Yoneda lemma shows that every WWyW \simeq W \star y, and if HH is cocontinuous then H(W)H(Wy)WHyH(W) \simeq H(W \star y) \simeq W \star H y, showing that the functor FFF \mapsto - \star F is essentially surjective. It is 2-fully-faithful by the universal property of colimits: a transformation FGF \to G gives rise to an essentially unique transformation FG-\star F \to -\star G.

Revision on June 14, 2011 at 15:15:33 by Finn Lawler?. See the history of this page for a list of all contributions to it.