Return to Answer

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.

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...

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 projective generator $P$. But 1) the compact projective 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.

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.

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 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. 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 use a characterization of categories monadic over $\text{Set}$ as the Barr exact categories with a compact projective generator $P$. But 1) the compact projective 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.

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 projective generator $P$. But 1) the compact projective 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.