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

Showing changes from revision #2 to #3: 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:J→KD \colon J \to K and W:J op→CatW \colon J^{op} \to Cat be pseudofunctors. Then

  1. The 2-colimit W⋆ J D W \star J D satisfies

    K(W⋆ J D,X)≃[J op,Cat](W,K(D−,X)) K(W \star J, 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⋆ p J D W \star_{p} J 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 s J D W \star^s_{p} J D satisfies

    K(W⋆ p s J D,X)≅Ps(J op,Cat)(W,K(D−,X)) K(W \star^s_p J, 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 s J D W \star^s_s J D satisfies

    K(W⋆ s s J D,X)≅Str(J op,Cat)(W,K(D−,X)) K(W \star^s_s J, 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 the bicategory in question is a strict 2-category, then for any index bicategory J K J K there is a strict 2-category 2-category, then for any index bicategoryJ′ J' J such there that is a strict functors 2-categoryJ′→K J' \to K are such the that same strict thing functors as pseudofunctorsJ′→K J J' \to K , and are the 2-colimit same of thing as pseudofunctors W J ⋆ → D K W J \star \to D K, and the 2-colimit of pseudofunctors W⋆DW \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 K = [K^{op}, Cat] is a strict 2-category, and it has all strict (CatCat-weighted) colimits, which are computed pointwise as usual for enriched functor categories: if now D:J→PKD \colon J \to P K and W:J op→CatW \colon J^{op} \to Cat are strict, then we can define (W⋆ s sD)a=W⋆ s sD(−,a)(W \star^s_s D) a = W \star^s_s D(-,a), and verify its universal property:

    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,PK(D−,F)) \array{ P K(W \star^s_s D, F) & \simeq \int_a Cat(W \star^s_s D(-,a), F a) \\ & \simeq \int_a Str(J^{op}, Cat)(W, Cat(D(-,a), F a)) \\ & \simeq Str(J^{op}, Cat)(W, P K(D-, F)) }

So PKP K has strict 2-colimits and hence also non-strict 2-colimits.

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]

For this we simply follow the usual reasoning: from left to right we compose with the Yoneda embedding y:K→PKy \colon K \to P K, and given a functor F:K→LF \colon K \to L we get a cocontinuous PK→LP K \to L sending W:K op→CatW \colon K^{op} \to Cat to W⋆FW \star F.

The co-Yoneda lemma shows that everyW≃W⋆yW \simeq W \star y, and if HH is cocontinuous then H(W)≃H(W⋆y)≃W⋆Hy H(W) \simeq H(W \star y) \simeq W \star H y, showing that the functor F↦− ∘ ⋆ y F F \mapsto - \circ \star y F is essentially surjective. It is 2-fully-faithful by the universal property of colimits: a transformation F→GF \to G gives rise to an essentially unique transformation −⋆F→−⋆G-\star F \to -\star G.

Revision on June 11, 2011 at 17:09:07 by Finn Lawler?. See the history of this page for a list of all contributions to it.