Axioms for the category of groups

Question

Certain categories of mathematical structures have had synthetic axiom systems developed for them. One particularly well known such category is the category of sets and functions $\mathit{Set}$, which was axiomatised by William Lawvere as the Elementary Theory of the Category of Sets. More recently, Michael Shulman came up with axioms for the dagger category of sets and relations $\mathit{Rel}$ in his theory Sets, Elements, and Relations, and Chris Heunen and Andre Kornell came up with axioms for the dagger category of (real, complex) Hilbert spaces and continuous linear maps $\mathit{Hilb}$ in their article Axioms for the category of Hilbert spaces. Has anybody developed a synthetic set of axioms for the category of groups $\mathit{Grp}$ yet?

Answer 1

This is not really in the spirit of the examples you give but it is at least a set of purely categorical properties.

Proposition: A category $C$ is the category of models of a Lawvere theory iff it has reflexive coequalizers and there exists an object $P$ (the free object on one generator) such that the functor $U = \text{Hom}(P, -) : C \to \text{Set}$ preserves sifted colimits, is conservative, and has a left adjoint $F : \text{Set} \to C$.

Sketch. Since reflexive coequalizers are sifted colimits, by the crude monadicity theorem the adjunction $F \vdash U$ is monadic, so $C$ is the category of algebras over the monad $UF : \text{Set} \to \text{Set}$. Since $UF$ preserves sifted colimits, and in particular preserves filtered colimits, it is a finitary monad, and these are known to be equivalent to (the monads induced by) Lawvere theories, with the equivalence also sending categories of algebras to categories of models. $\Box$

This set of categorical properties could be replaced by other ones, e.g. we could replace "has a left adjoint" with hypotheses sufficient for the adjoint functor theorem, and/or use a characterization of categories monadic over $\text{Set}$ as the Barr exact categories with a compact regular-projective generator $P$. But 1) the generator of the category of models of a Lawvere theory given by the free object on one generator always satisfies the stronger property above that $\text{Hom}(P, -)$ preserves sifted, not just filtered, colimits, and 2) because reflexive coequalizers are sifted colimits, this lets us apply the crude monadicity theorem without needing to know anything else about the behavior of coequalizers. So I think this characterization is a bit simpler.

Now $\text{Grp}$ can be isolated as the category satisfying the above properties such that the monad $UF$ is the free group monad. I don't expect this to be particularly satisfying but it does at least establish that $\text{Grp}$ can be isolated among all categories via categorical properties.

Edit: Philosophically I think the category of groups is less interesting to ask for a synthetic theory of compared to the examples you give of sets and Hilbert spaces. Sets and Hilbert spaces are both categories in which interesting stuff "takes place" while I don't think the category of groups is really like this. I think a more interesting question would be to ask for a synthetic theory of the $2$-category of groupoids, along the lines of homotopy type theory as a synthetic category of the $\infty$-category of $\infty$-groupoids. This is more of a "spatial" category, much closer in behavior to $\text{Set}$ (e.g. it is now distributive), and a category in which stuff can "take place."

The category of groups isn't that great anyway; some important constructions on groups cannot be understood in terms of it, e.g. the semidirect product and HNN extensions. The $2$-category of groupoids is capable of expressing both of these and more as homotopy colimits. It also naturally provides a home for the center, the outer automorphism group, the classification of arbitrary group extensions, the classification of projective representations...

Answer 2

As requested, here is an answer summarizing axioms for the category of groups that were given by Pierre Leroux, and which I learned from an MSE answer of Arnaud D. The category of groups is the unique category $C$ with the following properties:

1. It has all limits and colimits, and a zero object.
2. It has as a full subcategory $C_Z$ a category closed under coproducts and containing a cogroup $Z,$ and generated by the morphisms required by those properties.
3. $C_Z$ is closed under subobjects in $C.$
4. $Z$ is a regular-projective generator of $C.$
5. Every inclusion of the equivalence class of $0$ in an equivalence relation on an object of $C$ is a normal monomorphism.
6. Every object of $C$ is a subobject of a simple object.

Answer 3

The category of groups is the universal example of a cocomplete category equipped with a cogroup object. A similar statement holds for other types of algebraic structures. This is due to Freyd. See also my paper on limit sketches for a generalization.

This doesn't describe the category of groups internally of course, but rather by its relation to other cocomplete categories.

The category of sets is the cocomplete category freely generated by one object.