Read-back: finitely generated abelian groups have the packing property

The statement

Let $G$ be a set carrying the structure of a commutative group (a group whose multiplication satisfies $ab = ba$ for all $a, b \in G$; the group is written multiplicatively, with identity $1$). Assume in addition that $G$ is finitely generated: there exists a finite subset $T \subseteq G$ such that the smallest subgroup of $G$ containing $T$ is all of $G$. (Here "smallest subgroup containing $T$" means the intersection of all subgroups of $G$ that contain $T$.)

Then $G$ has the following property, which the declaration calls the packing property and which unfolds as follows.

For every finite subset $F \subseteq G$, there exist two subsets $S, X \subseteq G$ such that

1. $F \subseteq S$;
2. $S$ is finite;
3. the map

is a bijection from the Cartesian product $S \times X$ onto all of $G$.

Item 3, spelled out completely, is the conjunction of three conditions on the map $\mu(s,x) = s\cdot x$ restricted to pairs $(s,x)$ with $s \in S$ and $x \in X$:

• (maps into $G$) for every $s \in S$ and $x \in X$, the product $s \cdot x$ lies in $G$ — this condition is automatically true, since every element of $G$ lies in $G$;
• (injective on $S \times X$) for all $s, s' \in S$ and $x, x' \in X$, if $s \cdot x = s' \cdot x'$ then $(s, x) = (s', x')$, i.e. $s = s'$ and $x = x'$;
• (surjective onto $G$) every $g \in G$ is of the form $g = s \cdot x$ for some $s \in S$ and some $x \in X$.

So item 3 says exactly: every element of $G$ can be written as $s \cdot x$ with $s \in S$, $x \in X$, and this representation is unique. The product is taken in the order "element of $S$ on the left, element of $X$ on the right"; since $G$ is commutative here, the order does not change the value.

What is quantified, and how

• $G$ is universally quantified (it is an implicit parameter of the theorem) and ranges over types in an arbitrary universe. The two structural assumptions on $G$ — commutative group, finitely generated — are the only hypotheses.
• "Finitely generated" is stated for the group structure underlying the commutative-group structure: the finite generating set generates $G$ as a group (closure under multiplication and inverses), not merely as a monoid.
• Inside the conclusion, $F$ is universally quantified over all subsets of $G$, with the hypothesis that $F$ is finite. "Finite" means the subset is in bijection with $\{0, 1, \dots, n-1\}$ for some natural number $n$; the empty set counts as finite.
• $S$ and $X$ are existentially quantified (plain existence, not unique existence). They may depend on $F$. There is no finiteness requirement on $X$, and no other constraint on $X$ beyond item 3.
• The theorem asserts only that such $S$ and $X$ exist; it does not describe them, bound the size of $S$ in terms of $F$, or claim any uniqueness.

Edge cases the quantifiers silently include

• $F = \varnothing$. The empty set is finite, so the property must hold for it: some finite $S$ (which may be any finite set, since $\varnothing \subseteq S$ trivially) and some $X$ with $S \times X \to G$ bijective must exist.
• $S$ and $X$ cannot be empty. Item 3 requires surjectivity onto $G$, and $G$ contains the identity element $1$, so $G \ne \varnothing$; hence the product $S \times X$ must be nonempty, forcing both $S \ne \varnothing$ and $X \ne \varnothing$. This is a consequence of the definition, not a separate hypothesis.
• Nothing requires $1 \in S$ or $1 \in X$. The definition places no such condition.
• $F$ need not be a subgroup, need not contain $1$, and need not be closed under anything. It is an arbitrary finite subset.
• The trivial group $G = \{1\}$ is a commutative group generated by the empty set, so it is within the scope of the hypotheses.
• Every finite commutative group is finitely generated (by itself), so all finite commutative groups are in scope; so are, for example, $\mathbb{Z}^n$ and finite products of cyclic groups. Infinitely generated commutative groups (such as $\mathbb{Q}$ under addition) are not covered by the hypotheses.
• Non-commutative groups are not covered, even if finitely generated: commutativity is a hypothesis, not a conclusion.
• The hypotheses are satisfiable (e.g. by the trivial group), so the statement is not vacuous.

Summary in one sentence

For every finitely generated commutative group $G$ and every finite subset $F \subseteq G$, there is a finite set $S$ with $F \subseteq S \subseteq G$ and a (possibly infinite) set $X \subseteq G$ such that every element of $G$ is uniquely expressible as a product $s \cdot x$ with $s \in S$ and $x \in X$.