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?
-
2$\begingroup$ It's a semiabelian category, to start. One could wonder what special properties is has in addition that singles it out among those. $\endgroup$– David Roberts ♦Commented Oct 22, 2022 at 7:19
-
2$\begingroup$ One non-interesting possibility is to use a theorem of Kan that the category of cogroups in the category of groups is equivalent to the category of sets. So the axioms might be finite coproducts + the ETCS axioms on the category of internal cogroups. What seems to me interesting is which kind of categories are equivalent to the category of internal groups in the category of their internal cogroups. $\endgroup$– მამუკა ჯიბლაძეCommented Oct 22, 2022 at 11:27
-
1$\begingroup$ See also: Could groups be used instead of sets as a foundation of mathematics? $\endgroup$– Oscar CunninghamCommented Oct 22, 2022 at 13:23
-
4$\begingroup$ The most relevant answer I’ve seen appeared on MSE a few years back: math.stackexchange.com/questions/2332425/… $\endgroup$– Kevin CarlsonCommented Oct 22, 2022 at 22:31
-
1$\begingroup$ @KevinArlin can you write an answer summarising the axioms, pointing to the MSE post? $\endgroup$– David Roberts ♦Commented Oct 23, 2022 at 8:32
3 Answers
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:
- It has all limits and colimits, and a zero object.
- 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.
- $C_Z$ is closed under subobjects in $C.$
- $Z$ is a regular-projective generator of $C.$
- Every inclusion of the equivalence class of $0$ in an equivalence relation on an object of $C$ is a normal monomorphism.
- Every object of $C$ is a subobject of a simple object.
-
$\begingroup$ Thanks Kevin, this will allow the OP the chance to accept an actual answer to the question. $\endgroup$– David Roberts ♦Commented Oct 23, 2022 at 20:36
-
$\begingroup$ This is a very neat answer but it somehow smuggles in groups through that $Z$... $\endgroup$ Commented Oct 27, 2022 at 7:22
-
1$\begingroup$ @მამუკაჯიბლაძე Yes, though to be fair, characterizations of the category of sets also involve assuming the terminal object is a co-set object! Anyway I do think things like the characterization of categories of Hilbert spaces mentioned in the OP are strictly "better" than this one for that reason. $\endgroup$ Commented Oct 27, 2022 at 16:58
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...
-
2$\begingroup$ Groupoids are the types that satisfy UIP, so we know how to give a type-theoretic account of them, which however is not in the spirit of the question. $\endgroup$ Commented Oct 22, 2022 at 9:33
-
1$\begingroup$ There is actually some litterature about interpreting classical group construction in terms of the category of groups, and other interesting properties of the category of groups. Like a category theoretic account of the Automorphism group of a group, or semi-direct product. This is studied by people working with things like protomodular, semi-abelian, or Mal'cev categories. I'm not very familiar with these topic but this book link.springer.com/book/10.1007/978-1-4020-1962-3 is probably a good starting place - chapter 5 has a discussion of semi-direct product. $\endgroup$ Commented Nov 9, 2022 at 16:40
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.
