Let $\mathcal{C}$ be a category.
-
Functoriality. The assignment $\mathcal{C}\mapsto \mathrm{K}_{0}\webleft (\mathcal{C}\webright )$ defines a functor
\[ \mathrm{K}_{0} \colon \mathsf{Cats}\to \mathsf{Grpd}. \]
-
2-Functoriality. The assignment $\mathcal{C}\mapsto \mathrm{K}_{0}\webleft (\mathcal{C}\webright )$ defines a 2-functor
\[ \mathrm{K}_{0} \colon \mathsf{Cats}_{\mathsf{2}}\to \mathsf{Grpd}_{\mathsf{2}}. \]
-
Adjointness. We have an adjunction witnessed by a bijection of sets
\[ \textup{Hom}_{\mathsf{Grpd}}\webleft (\mathrm{K}_{0}\webleft (\mathcal{C}\webright ),\mathcal{G}\webright )\cong \textup{Hom}_{\mathsf{Cats}}\webleft (\mathcal{C},\mathcal{G}\webright ), \]natural in $\mathcal{C}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$ and $\mathcal{G}\in \text{Obj}\webleft (\mathsf{Grpd}\webright )$, forming, together with the functor $\mathsf{Core}$ of Item 1 of Proposition 8.3.3.1.4, a triple adjunction
witnessed by bijections of sets
\begin{align*} \textup{Hom}_{\mathsf{Grpd}}\webleft (\mathrm{K}_{0}\webleft (\mathcal{C}\webright ),\mathcal{G}\webright ) & \cong \textup{Hom}_{\mathsf{Cats}}\webleft (\mathcal{C},\mathcal{G}\webright ),\\ \textup{Hom}_{\mathsf{Cats}}\webleft (\mathcal{G},\mathcal{D}\webright ) & \cong \textup{Hom}_{\mathsf{Grpd}}\webleft (\mathcal{G},\mathsf{Core}\webleft (\mathcal{D}\webright )\webright ),\end{align*}natural in $\mathcal{C},\mathcal{D}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$ and $\mathcal{G}\in \text{Obj}\webleft (\mathsf{Grpd}\webright )$.
-
2-Adjointness. We have a 2-adjunction witnessed by an isomorphism of categories
\[ \mathsf{Fun}\webleft (\mathrm{K}_{0}\webleft (\mathcal{C}\webright ),\mathcal{G}\webright )\cong \mathsf{Fun}\webleft (\mathcal{C},\mathcal{G}\webright ), \]natural in $\mathcal{C}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$ and $\mathcal{G}\in \text{Obj}\webleft (\mathsf{Grpd}\webright )$, forming, together with the 2-functor $\mathsf{Core}$ of Item 2 of Proposition 8.3.3.1.4, a triple 2-adjunction
witnessed by isomorphisms of categories
\begin{align*} \mathsf{Fun}\webleft (\mathrm{K}_{0}\webleft (\mathcal{C}\webright ),\mathcal{G}\webright ) & \cong \mathsf{Fun}\webleft (\mathcal{C},\mathcal{G}\webright ),\\ \mathsf{Fun}\webleft (\mathcal{G},\mathcal{D}\webright ) & \cong \mathsf{Fun}\webleft (\mathcal{G},\mathsf{Core}\webleft (\mathcal{D}\webright )\webright ),\end{align*}natural in $\mathcal{C},\mathcal{D}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$ and $\mathcal{G}\in \text{Obj}\webleft (\mathsf{Grpd}\webright )$.
-
Interaction With Classifying Spaces. We have an isomorphism of groupoids
\[ \mathrm{K}_{0}\webleft (\mathcal{C}\webright ) \cong \Pi _{\leq 1}\webleft (\left\lvert \mathrm{N}_{\bullet }\webleft (\mathcal{C}\webright )\right\rvert \webright ), \]
natural in $\mathcal{C}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$; i.e. the diagram
commutes up to natural isomorphism.
-
Symmetric Strong Monoidality With Respect to Coproducts. The groupoid completion functor of Item 1 has a symmetric strong monoidal structure
\[ \webleft (\mathrm{K}_{0},\mathrm{K}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{0},\mathrm{K}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{0|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Cats},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset _{\mathsf{cat}}\webright ) \to \webleft (\mathsf{Grpd},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset _{\mathsf{cat}}\webright ) \]
being equipped with isomorphisms
\[ \begin{gathered} \mathrm{K}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{0|\mathcal{C},\mathcal{D}} \colon \mathrm{K}_{0}\webleft (\mathcal{C}\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\mathrm{K}_{0}\webleft (\mathcal{D}\webright ) \xrightarrow {\cong }\mathrm{K}_{0}\webleft (\mathcal{C}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}\mathcal{D}\webright ),\\ \mathrm{K}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{0|\mathbb {1}} \colon \emptyset _{\mathsf{cat}}\xrightarrow {\cong }\mathrm{K}_{0}\webleft (\emptyset _{\mathsf{cat}}\webright ), \end{gathered} \]natural in $\mathcal{C},\mathcal{D}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$.
-
Symmetric Strong Monoidality With Respect to Products. The groupoid completion functor of Item 1 has a symmetric strong monoidal structure
\[ \webleft (\mathrm{K}_{0},\mathrm{K}^{\times }_{0},\mathrm{K}^{\times }_{0|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Cats},\times ,\mathsf{pt}\webright ) \to \webleft (\mathsf{Grpd},\times ,\mathsf{pt}\webright ) \]
being equipped with isomorphisms
\[ \begin{gathered} \mathrm{K}^{\times }_{0|\mathcal{C},\mathcal{D}} \colon \mathrm{K}_{0}\webleft (\mathcal{C}\webright )\times \mathrm{K}_{0}\webleft (\mathcal{D}\webright ) \xrightarrow {\cong }\mathrm{K}_{0}\webleft (\mathcal{C}\times \mathcal{D}\webright ),\\ \mathrm{K}^{\times }_{0|\mathbb {1}} \colon \mathsf{pt}\xrightarrow {\cong }\mathrm{K}_{0}\webleft (\mathsf{pt}\webright ), \end{gathered} \]natural in $\mathcal{C},\mathcal{D}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$.
