Read-back: six definitions

Throughout, "group" means a type together with a group structure on it (an associative multiplication with a two-sided identity $1$ and two-sided inverses). Four of the six definitions below place no constraint at all on the universe the group lives in. The first and the last are stated at a fixed universe level $u$; there the restriction that matters is an internal one — certain auxiliary types are required to lie in the same universe as the group — and it is recorded where it bites.

Two conventions recur and are stated once here.

Subgroups. A subgroup of a group $G$ is a subset of $G$ containing $1$ and closed under products and under inverses. A subgroup is again a group, under the multiplication inherited from $G$; whenever a subgroup appears below in a position where a group is wanted, it is that inherited structure that is meant. Subgroups of $G$ are ordered by inclusion of their underlying subsets, and $\top$ denotes the subgroup whose underlying subset is all of $G$. For a family $(H_i)_{i \in \iota}$ of subgroups, $\bigsqcup_{i} H_i$ denotes their supremum in this order: the smallest subgroup of $G$ containing every $H_i$, equivalently the subgroup generated by $\bigcup_i H_i$. It is in general larger than the set-theoretic union $\bigcup_i H_i$, and coincides with it when $\iota$ is non-empty and the family is directed. The supremum of the empty family is the trivial subgroup $\{1\}$.

Quotients. A subgroup $N \le G$ is normal when $g n g^{-1} \in N$ for every $n \in N$ and every $g \in G$. For any subgroup $N$, the symbol $G/N$ denotes the set of left cosets of $N$ (the quotient of $G$ by the relation $x \sim y \iff x^{-1} y \in N$). When $N$ is normal, $G/N$ carries the induced group multiplication, and it is that group that is meant whenever $G/N$ appears below in a position where a group is wanted. The normality hypothesis is therefore not decoration: it is what makes the quotient symbol denote a group at all.

Also: a type is called finite when there is a bijection between it and $\{0, 1, \dots, n-1\}$ for some natural number $n$ (so $n = 0$, i.e. an empty type, is allowed for a type in general, though not for a group, which contains $1$). A subset $S$ of a type is called finite when the type of elements of $S$ is finite in this sense.

---

1. Constructible

Fix once and for all a universe level $u$. The definition introduces a property

$$\mathrm{Constructible}(G, \ast)$$

of pairs consisting of a type $G$ lying in the universe $u$ and a group structure $\ast$ on $G$. Both the type and the group structure are arguments of the property: it is a property of groups, not of underlying types, and two different group structures on the same type are two different instances of it. Below, "the group $G$ is constructible" always means this property holds of $G$ together with the group structure under discussion.

The property is defined inductively: it is the smallest property of such pairs that is closed under the five rules below. Concretely, this amounts to two assertions.

(a) Each of the five rules holds.

Rule 1 (finite groups). Let $G$ be any type in universe $u$, with any group structure on it. If the type $G$ is finite, then $G$ is constructible.

Rule 2 (commutative groups). Let $G$ be any type in universe $u$ carrying a commutative group structure. Then $G$, equipped with the group structure underlying that commutative structure, is constructible. There is no finiteness, countability or generation hypothesis of any kind here.

Rule 3 (transport along an isomorphism). Let $G$ and $H$ both be types in the universe $u$, each with a group structure, and let $e$ be a group isomorphism from $G$ to $H$ — that is, a bijection $e : G \to H$ satisfying $e(x y) = e(x)\, e(y)$ for all $x, y \in G$. If $G$ is constructible, then $H$ is constructible. The rule is stated in this one direction, from the source of $e$ to its target, and it requires $G$ and $H$ to lie in the same universe $u$; there is no rule transporting the property to a group in a different universe.

Rule 4 (extensions). Let $G$ be a group (type in universe $u$), let $N$ be a subgroup of $G$, and suppose $N$ is normal in $G$. If $N$ — as a group, under the multiplication inherited from $G$ — is constructible, and the quotient group $G/N$ is constructible, then $G$ is constructible. Both halves are required; neither alone triggers the rule.

Rule 5 (directed unions). Let $G$ be a group (type in universe $u$), let $\iota$ be a type lying in the same universe $u$, and let $H : \iota \to \{\text{subgroups of } G\}$ be a family of subgroups of $G$ indexed by $\iota$. Suppose:

• (directedness) for every $i, j \in \iota$ there exists $k \in \iota$ with $H_i \subseteq H_k$ and $H_j \subseteq H_k$; and
• (exhaustion) $\bigsqcup_{i \in \iota} H_i = \top$, i.e. the smallest subgroup of $G$ containing every $H_i$ is $G$ itself; and
• $H_i$, as a group under the inherited multiplication, is constructible for every $i \in \iota$.

Then $G$ is constructible.

Two features of Rule 5 are worth spelling out. First, the index type $\iota$ is constrained to the same universe as $G$; a family indexed by a type from a larger universe is not covered. Second, the exhaustion hypothesis is an equation between subgroups about the supremum, not about the union; with directedness and $\iota$ non-empty these agree, but the hypothesis as written is the statement about the supremum.

Degenerate case of Rule 5. Nothing requires $\iota$ to be non-empty. If $\iota$ is empty, directedness holds vacuously, the family of constructibility hypotheses is vacuous, and the supremum of the empty family is the trivial subgroup, so the exhaustion hypothesis reads "$\{1\} = G$". Thus in the empty-index case Rule 5 reads: every group whose only element is the identity is constructible.

(b) Nothing else is constructible. Equivalently — and this is the induction principle that the inductive definition provides — let $P(G, \ast)$ be any property of (type in universe $u$, group structure) pairs. Suppose that $P$ satisfies the analogues of all five rules above, where in Rules 3, 4 and 5 one may assume both that the smaller groups are constructible and that $P$ holds of them (for Rule 5, that $P(H_i)$ holds for every $i \in \iota$). Then $P(G, \ast)$ holds for every constructible group $G$.

In particular, a group is constructible precisely when it admits a well-founded derivation whose steps are instances of Rules 1–5.

Finally, note which closure rules are not among the five: there is no rule concluding that a subgroup of a constructible group is constructible, and no rule concluding that a quotient of a constructible group by a normal subgroup is constructible. Rule 4 uses constructibility of a normal subgroup and of the corresponding quotient as hypotheses, in the direction of building $G$ up; it does not run the other way.

---

2. Locally finite

Let $G$ be a group (in any universe). The property $G$ is locally finite asserts:

for every subset $S \subseteq G$, if $S$ is finite, then the subgroup of $G$ generated by $S$ is a finite type.

Here "the subgroup generated by $S$" means the intersection of all subgroups of $G$ that contain $S$ — equivalently the smallest subgroup containing $S$ — and "is a finite type" means that the set of elements of that subgroup is in bijection with $\{0, 1, \dots, n-1\}$ for some natural number $n$.

The quantification is over all finite subsets, with no side condition. In particular $S = \varnothing$ is included, where the generated subgroup is the trivial subgroup $\{1\}$; and one-element subsets $S = \{g\}$ are included, where the instance reads "the subgroup generated by $g$ is finite". Note that the conclusion is about subgroups generated by finite subsets of $G$; it says nothing directly about subgroups of $G$ presented in any other way.

---

3. No free subgroup of rank two

Let $G$ be a group (in any universe). Let $F$ denote the free group on a two-element index set $\{0, 1\}$: the group of reduced words in two generators and their formal inverses, with concatenation-then-reduction as multiplication, characterised by the universal property that every function from $\{0,1\}$ into a group $H$ extends uniquely to a group homomorphism $F \to H$.

The property asserted is:

for every group homomorphism $f : F \to G$, the underlying function of $f$ is not injective.

"Homomorphism" here means a map preserving multiplication and sending $1$ to $1$, and "not injective" means: it is not the case that $f(w_1) = f(w_2)$ implies $w_1 = w_2$ for all $w_1, w_2 \in F$ — i.e. there exist two distinct elements of $F$ with the same image.

The statement is a universally quantified negation, one homomorphism at a time. It is phrased in terms of homomorphisms out of $F$, not in terms of subgroups of $G$; the trivial homomorphism is among those quantified over.

---

4. Packing

Let $G$ be a group (in any universe) and let $S$ and $X$ be two subsets of $G$, given in that order. The property $(S, X)$ is a packing asserts that the multiplication map

$$(s, x) \;\longmapsto\; s \cdot x$$

restricted to the set of pairs $\{(s,x) : s \in S,\ x \in X\} \subseteq G \times G$, is a bijection from that set of pairs onto all of $G$. Unfolded, this is the conjunction of three clauses:

1. (image clause) every product $s \cdot x$ with $s \in S$, $x \in X$ lies in $G$. The target set here is all of $G$, so this clause carries no information; it holds for every $S$ and $X$.

2. (injectivity) for all $s, s' \in S$ and all $x, x' \in X$, if $s \cdot x = s' \cdot x'$ then $s = s'$ and $x = x'$.

3. (surjectivity) for every $g \in G$ there exist $s \in S$ and $x \in X$ with $s \cdot x = g$.

So the content is: every element of $G$ can be written as $s x$ with $s \in S$ and $x \in X$, and in exactly one way. The order of the factors is fixed — the element of $S$ is on the left and the element of $X$ on the right — and the two arguments are not interchangeable in the statement.

Neither $S$ nor $X$ is required to be finite, to be non-empty, or to be a subgroup, or to contain $1$. Note, however, that clause 3 applied to $g = 1$ cannot be met if either $S$ or $X$ is empty, so emptiness of either set is incompatible with the property.

---

5. Has the packing property

Let $G$ be a group (in any universe). The property $G$ has the packing property asserts:

for every subset $F \subseteq G$, if $F$ is finite, then there exist subsets $S, X \subseteq G$ such that $F \subseteq S$, and $S$ is finite, and $(S, X)$ is a packing of $G$ in the sense of §4 — i.e. every element of $G$ factors as $s x$ with $s \in S$, $x \in X$, uniquely.

Points of precision:

• The containment demanded is $F \subseteq S$, with $S$ the left-hand factor of the packing. Nothing is demanded of $F$ relative to $X$.
• $S$ is required to be finite; $X$ is subject to no cardinality or structural requirement whatsoever (though, as noted in §4, the packing condition forces $X$ to be non-empty).
• Neither $S$ nor $X$ is required to be a subgroup, or to contain $1$.
• Both $S$ and $X$ are existentially quantified after $F$, so they may depend on $F$.
• The case $F = \varnothing$ is included.

---

6. Residually elementary amenable

Let $G$ be a group (in any universe). The property asserted is:

for every $x \in G$ with $x \neq 1$, there exists a subgroup $K$ of $G$, and a proof that $K$ is normal in $G$, such that $x \notin K$ and the quotient group $G/K$ is elementary amenable.

Here the quotient $G/K$ is a group by virtue of the normality of $K$ just supplied, and the elementary amenability asserted is that of $G/K$ with that induced group structure.

The subgroup $K$ is quantified inside the quantifier over $x$, so it may depend on $x$. Since $x \in G$ and $x \notin K$, the subgroup $K$ is necessarily proper; but $K$ is not required to be trivial, nor to have any other property beyond being normal and omitting $x$. If $G$ has only the identity element, the hypothesis $x \neq 1$ can never be met and the whole condition holds vacuously.

What "elementary amenable" unfolds to

The property invoked is itself an inductive one. As with the property of §1, it is fixed at a universe level $u$ and is a property of a type in universe $u$ together with a group structure on it; the quotient $G/K$ lies in the same universe as $G$, so this costs nothing here. It is the smallest property of such pairs closed under the following seven rules:

1. (finite) if the type $G$ is finite, then $G$ is elementary amenable;
2. (commutative) if $G$ carries a commutative group structure, then $G$ with the underlying group structure is elementary amenable;
3. (transport) if $G$ and $H$ lie in the same universe $u$, $e : G \to H$ is a bijection with $e(xy) = e(x) e(y)$, and $G$ is elementary amenable, then $H$ is elementary amenable;
4. (subgroups) if $G$ is elementary amenable and $H$ is any subgroup of $G$, then $H$, with the inherited multiplication, is elementary amenable;
5. (quotients) if $G$ is elementary amenable and $N$ is a normal subgroup of $G$, then the quotient group $G/N$ is elementary amenable;
6. (extensions) if $N$ is a normal subgroup of $G$ such that $N$ is elementary amenable and $G/N$ is elementary amenable, then $G$ is elementary amenable;
7. (directed unions) if $\iota$ is a type in the same universe $u$ as $G$ and $(H_i)_{i \in \iota}$ is a family of subgroups of $G$ such that for all $i, j$ there is $k$ with $H_i \subseteq H_k$ and $H_j \subseteq H_k$, such that $\bigsqcup_{i} H_i = \top$ (the smallest subgroup containing all $H_i$ is $G$), and such that every $H_i$ is elementary amenable, then $G$ is elementary amenable.

As in §1, "smallest" means additionally that any property of (type, group structure) pairs closed under these seven rules holds of every elementary amenable group, and that the empty index type in rule 7 is permitted, in which case the exhaustion hypothesis reads "$\{1\} = G$".

So, written out in full, §6 says: for every non-identity $x \in G$ there is a normal subgroup $K$ of $G$ with $x \notin K$ such that $G/K$ can be derived, by a well-founded derivation using rules 1–7 above, as an elementary amenable group.