As we all know, the forgetful functor $\mathsf{Ab} \to \mathsf{CMon}$ from abelian groups to commutative monoids has a left adjoint, the **Grothendieck group**. I would like to **categorify** this construction.

For this, abelian groups should be replaced by symmetric monoidal categories in which every object is invertible, let's call them abelian $2$-groups (notice that $2$-groups usually are assumed to be groupoids; if possible I would like to avoid this assumption). And commutative monoids are replaced by symmetric monoidal categories. We have a forgetful functor of $2$-categories $\mathsf{2Ab} \to \mathsf{2CMon}$. I am pretty sure that it has a left adjoint (in the $2$-categorical sense) and how it looks like, but it is quite tedious to verify all the details. Therefore I would like to know if this construction is already known (probably!) and if it has been written down somewhere, so that I may cite it.

Here is a sketch of the construction: Given a symmetric monoidal category $S$, whose tensor product will be denoted simply by $(a,b) \mapsto ab$, we define a symmetric monoidal category $S^{-1} S$ as follows (not to be confused with Quillen's $S^{-1} S$!): Objects are pairs of objects of $S$. One should think of $(a,b)$ as $a^{-1} b$. A morphism $(a,b) \to (c,d)$ is an equivalence class of morphisms $ebc \to ead$ for objects $e$, where two such morphisms $ebc \to ead$, $fbc \to fad$ are called equivalent if there are objects $e',f'$ and an isomorphism $e'e \to f'f$ such that $$\begin{array}{c} e'ebc & \rightarrow & e'ead \\ \downarrow && \downarrow \\ f'fbc & \rightarrow & f'fad \end{array}$$ commutes. The composition of morphisms is a little bit long, but is motivated by the transitivity proof in the construction of the usual Grothendieck group (one also has to check the category axioms ...). The tensor product is $(a,b) (c,d) := (ca,bd)$ on objects (one also has to define it on morphisms ...), the unit is $(1,1)$. Then $(a,b) (b,a) = (ba,ba) \cong (1,1)$ shows that every object is invertible. One has a symmetric monoidal functor $\iota : S \to S^{-1} S$, $a \mapsto (1,a)$. If $F : S \to T$ is a symmetric monoidal functor and every object of $T$ is invertible, then there is a symmetric monoidal functor $\tilde{F} : S^{-1} S \to T$ with $\tilde{F}(a,b) = F(a)^{-1} F(b)$ (one also has to define $\tilde{F}$ on morphisms and check the coherence diagrams ...) and this construction (probably ...) establishes an equivalence of categories $\hom(S,T) \cong \hom(S^{-1} S,T)$. Notice that if $S$ is discrete, $S$ is just a commutative monoid and $S^{-1} S$ is the usual Grothendieck group of $S$.

nontrivialisos $b a^{-1} = a^{-1} b$, which allow you to build a path $a_1^{-1} b_1 \dots a_n^{-1} b_n = a^-1 b$, $a = a_1 \dots a_n$, $b = b_1 \dots b_n$. Thus you can get ahomotopy equivalencewith category of pairs $a^{-1} b$ withsome very complexmorphisms, and the multiplication is at best homotopy equivalent to the one you would want to write. $\endgroup$7more comments