Return to Answer

Let me elaborate on my comment. I think freeness is a red herring. The content of the standard topological proof is that a covering space of a $1$-dimensional CW complex is again a $1$-dimensional CW complex. Of course this naturally generalizes to the case where $1$ is replaced by any positive integer $k$, which suggests the following definition: say that a group $G$ has homotopy dimension at most $k$ if $BG$ can be presented by a $k$-dimensional CW complex. Then the same argument about covering spaces shows that every subgroup of a group with homotopy dimension at most $k$ again has homotopy dimension at most $k$. Homotopy dimension at most $1$ is equivalent to freeness in the presence of choice, but using it instead of freeness in the argument removes the need to choose a spanning tree and that should address concerns about uses of choice.

As the long list of examples in Todd's answer also suggests, we should be looking at some property other than freeness in general. I think some kind of cohomological dimension is a better candidate; as stated in Matthias Wendt's comment below, the nontrivial free groups are precisely the groups of cohomological dimension $1$.

Let me elaborate on my comment. I think freeness is a red herring. The content of the standard topological proof is that a covering space of a $1$-dimensional CW complex is again a $1$-dimensional CW complex. Of course this naturally generalizes to the case where $1$ is replaced by any positive integer $k$, which suggests the following definition.

Say that a group $G$ has homotopy dimension at most $k$ if $BG$ can be presented by a $k$-dimensional CW complex (e.g. take $BG$ to be a compact hyperbolic $k$-manifold). Then the same argument about covering spaces shows that every subgroup of a group with homotopy dimension at most $k$ again has homotopy dimension at most $k$. Homotopy dimension at most $1$ is equivalent to freeness in the presence of choice, but using it instead of freeness in the argument removes the need to choose a spanning tree and that should address concerns about uses of choice.

As the long list of examples in Todd's answer also suggests, we should be looking at some property other than freeness in general. I think some kind of cohomological dimension is a better candidate; as stated in Matthias Wendt's comment below, the nontrivial free groups are precisely the groups of cohomological dimension $1$. And $1$-dimensionality also shows up in Ben Webster's answer.

Let me elaborate on my comment. I think freeness is a red herring. If you look at the standard topological proof the content of the proof is that a covering space of a $1$-dimensional CW complex is again a $1$-dimensional CW complex. Of course this naturally generalizes to the case where $1$ is replaced by any positive integer $k$, which suggests the following definition: say that a group $G$ has property $F_k$ if $BG$ can be presented by a $k$-dimensional CW complex. Then the same argument about covering spaces shows that every subgroup of a group with property $F_k$ again has property $F_k$. Property $F_1$ is equivalent to freeness but using it instead of freeness in the argument removes the need to choose a spanning tree and that should address concerns about uses of choice.

As the long list of examples in Todd's answer also suggests, we should be looking at some property other than freeness in general. I think some kind of cohomological dimension is a better candidate; I believe it's known in particular that free groups are also precisely the groups of cohomological dimension $1$.

Let me elaborate on my comment. I think freeness is a red herring. The content of the standard topological proof is that a covering space of a $1$-dimensional CW complex is again a $1$-dimensional CW complex. Of course this naturally generalizes to the case where $1$ is replaced by any positive integer $k$, which suggests the following definition: say that a group $G$ has homotopy dimension at most $k$ if $BG$ can be presented by a $k$-dimensional CW complex. Then the same argument about covering spaces shows that every subgroup of a group with homotopy dimension at most $k$ again has homotopy dimension at most $k$. Homotopy dimension at most $1$ is equivalent to freeness in the presence of choice, but using it instead of freeness in the argument removes the need to choose a spanning tree and that should address concerns about uses of choice.

As the long list of examples in Todd's answer also suggests, we should be looking at some property other than freeness in general. I think some kind of cohomological dimension is a better candidate; as stated in Matthias Wendt's comment below, the nontrivial free groups are precisely the groups of cohomological dimension $1$.

Let me elaborate on my comment. I think freeness is a red herring. If you look at the standard topological proof the content of the proof is that a covering space of a $1$-dimensional CW complex is again a $1$-dimensional CW complex. Of course this naturally generalizes to the case where $1$ is replaced by any positive integer $k$, which suggests the following definition: say that a group $G$ has property $F_k$ if $BG$ can be presented by a $k$-dimensional CW complex. Then the same argument about covering spaces shows that every subgroup of a group with property $F_k$ again has property $F_k$. Property $F_1$ is equivalent to freeness but using it instead of freeness in the argument removes the need to choose a spanning tree and that should address any possible concerns about uses of choice.

As the long list of examples in Todd's answer also suggests, we should be looking at some property other than freeness in general. I think some kind of cohomological dimension is a better candidate; in particular I believe it's known in particular that free groups are also precisely the groups of cohomological dimension $1$.

Let me elaborate on my comment. I think freeness is a red herring. If you look at the standard topological proof the content of the proof is that a covering space of a $1$-dimensional CW complex is again a $1$-dimensional CW complex. Of course this naturally generalizes to the case where $1$ is replaced by any positive integer $k$, which suggests the following definition: say that a group $G$ has property $F_k$ if $BG$ can be presented by a $k$-dimensional CW complex. Then the same argument about covering spaces shows that every subgroup of a group with property $F_k$ again has property $F_k$. Property $F_1$ is equivalent to freeness but using it instead of freeness in the argument removes the need to choose a spanning tree and that should address concerns about uses of choice.

As the long list of examples in Todd's answer also suggests, we should be looking at some property other than freeness in general. I think some kind of cohomological dimension is a better candidate; I believe it's known in particular that free groups are also precisely the groups of cohomological dimension $1$.