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

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

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

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

1. The 2-colimit $W \star D$ satisfies

   $$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 $K$ is a strict 2-category, the pseudocolimit $W \star_{p} D$ satisfies the same property up to isomorphism.

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

   $$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 \star^s_s D$ satisfies

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

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

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

1. $Cat$ is strictly 2-cocomplete: its underlying 1-category has small colimits, and $Cat$ is enriched and tensored over itself, so that it has strict $Cat$-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 $K$ is a strict 2-category, then for any index bicategory $J$ there is a strict 2-category $J'$ such that strict functors $J' \to K$ are the same thing as pseudofunctors $J \to K$, and the 2-colimit of pseudofunctors $W \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^{\mathrm{op}},\mathrm{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$\mathrm{<span><del\; class="diffmod">\; Cat</del><ins\; class="diffmod">\; P</ins></span>}K$ Cat P K -weighted) colimits, which are computed pointwise as usual for enriched strictly-enriched functor categories: if now$D \colon J \to P K$ and $W \colon J^{op} \to Cat$ are strict, then we set can define$(W{\star }_s^s\star D)a=W{\star }_s^s\star D(-,a)$ (W \star^s_s \star D) a = W \star^s_s \star D(-,a) , and verify its universal property: property follows:

   $$\begin{array}{cc}PK(W{\star }_s^s\star D,F)& \simeq {\int }_a\mathrm{Cat}(W{\star }_s^s\star D(-,a),Fa)\\ & \simeq {\int }_a\mathrm{Str}[(J^{\mathrm{op}},\mathrm{Cat}<span><del\; class="diffmod">\; )</del><ins\; class="diffmod">\; ]</ins></span>(W,\mathrm{Cat}(D(-,a),Fa))\\ & \simeq \mathrm{Str}[(J^{\mathrm{op}},\mathrm{Cat}<span><del\; class="diffmod">\; )</del><ins\; class="diffmod">\; ]</ins></span>(W,P{\int }_a\mathrm{<span><del\; class="diffmod">\; K</del><ins\; class="diffmod">\; Cat</ins></span>}(D<span><del\; class="diffmod">\; -</del><ins\; class="diffmod">\; (</ins></span>-,a),Fa))\\ & \simeq [J^{\mathrm{op}},\mathrm{Cat}](W,PK(D-,F))\end{array}$$ \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 $P K$ has 2-colimits.

So Finally, we need to show that if$\mathrm{<span><del\; class="diffmod">\; P</del><ins\; class="diffmod">\; L</ins></span>}K$ P L K has is strict a 2-colimits cocomplete and bicategory, hence then also there non-strict is 2-colimits. a 2-equivalence