Read-back

The declaration is a single closed statement. It has no variables, no hypotheses and no typeclass assumptions of its own: nothing is quantified over, and there is nothing to satisfy before it applies. Everything it speaks about is fixed by the definitions it names. Its content is one existence claim, which the rest of this note unpacks in full.

What the statement asserts, in one sentence

Writing $F$ for the group defined below and $F^{\mathrm{ab}}$ for its abelianization, the statement asserts:

$$\text{there exists at least one multiplication-preserving bijection } \varphi : F^{\mathrm{ab}} \longrightarrow \mathbb{Z} \times \mathbb{Z},$$

where $\mathbb{Z} \times \mathbb{Z}$ is the set of ordered pairs of integers with the group operation $(a,b) \cdot (c,d) = (a+c,\ b+d)$, that operation being written multiplicatively. Equivalently: $F^{\mathrm{ab}}$ is isomorphic, as a group, to the free abelian group of rank $2$.

The claim is purely existential. It exhibits no particular isomorphism, says nothing about where any specific element of $F^{\mathrm{ab}}$ is sent, and asserts no naturality, canonicity or uniqueness: it says only that the collection of such isomorphisms is not empty.

The ambient group

Let

$$I \;=\; \{\, x \in \mathbb{R} \;:\; 0 \le x \le 1 \,\},$$

regarded as a set in its own right and ordered by the order it inherits from $\mathbb{R}$ (so $u \le v$ in $I$ means exactly $u \le v$ in $\mathbb{R}$).

Let $G$ be the set of order isomorphisms of $I$. An element of $G$ is a package consisting of

• a map $f : I \to I$,
• a map $f^{-1} : I \to I$,
• the two round-trip identities $f^{-1}(f(u)) = u$ and $f(f^{-1}(v)) = v$ for all $u, v \in I$, and
• the equivalence $f(u) \le f(v) \iff u \le v$, for all $u,v \in I$.

No continuity, differentiability or measurability is required: an order isomorphism here is an order-theoretic object, not a topological one. (Since $I$ is a linearly ordered interval, the order condition does of course constrain $f$ strongly; the point is only that no topological hypothesis is written down.)

$G$ is a group under composition, with

$$(f \cdot g)(x) \;=\; f\bigl(g(x)\bigr),$$

with the identity map as neutral element and with $f^{-1}$ as the inverse of $f$. The order of composition is worth recording: in a product, the right factor is applied first.

Dyadic rationals

A real number $x$ is called dyadic when there are an integer $m$ and a natural number $k$ (with $k = 0$ allowed) such that

$$x \;=\; \frac{m}{2^{k}}.$$

So the dyadic numbers include all integers, and include negative numbers; they are not restricted to $[0,1]$.

The generating condition

Call an element $f \in G$ piecewise dyadic-linear when the following holds:

There exists a finite set $B \subseteq \mathbb{R}$ such that

1. every element of $B$ is dyadic, and
2. for all $x, y \in I$ with $x < y$ and

$$(x,y) \cap B \;=\; \varnothing$$

(the open interval from $x$ to $y$ meets $B$ in no point), there exist an integer $n \in \mathbb{Z}$ and a real number $c \in \mathbb{R}$ such that

$$f(z) \;=\; 2^{n} z + c \qquad \text{for every } z \in I \text{ with } x \le z \le y.$$

Several features of this condition affect what it says, and are recorded here rather than smoothed over.

• The set $B$ is existentially quantified, finite, and required only to consist of dyadic numbers. It is not required to be contained in $[0,1]$, nor to be the exact set of points where $f$ fails to be linear; any finite dyadic set with the stated property will do. The empty set is permitted, in which case the condition demands a single formula $2^n z + c$ valid on all of $I$ at once.
• The exponent $n$ and the intercept $c$ are quantified inside the "for all $x,y$", so they may differ from one interval to the next. That is what makes the condition a piecewise one.
• The slope is $2^{n}$ with $n$ an integer, not a natural number: it is a positive power of two and may be less than $1$ (e.g. $1/2$, $1/4$), but it is always strictly positive. Slope $0$ and negative slopes are excluded.
• The intercept $c$ is an arbitrary real number. Nothing in this condition requires $c$ to be dyadic, or rational.
• The affine identity is imposed on the closed interval $x \le z \le y$, endpoints included, and only for those $z$ that also lie in $I$.

The group $F$

Let

$$S \;=\; \{\, f \in G \;:\; f \text{ is piecewise dyadic-linear} \,\}$$

and let

$$F \;=\; \langle S \rangle$$

be the subgroup of $G$ generated by $S$: the smallest subgroup of $G$ containing $S$, equivalently the intersection of all subgroups of $G$ that contain $S$, equivalently the set of all finite products of elements of $S$ and of their inverses (together with the empty product, the identity).

$F$ is the generated subgroup, not the set $S$ itself. Nothing in the definitions used by this statement asserts that $S$ is already closed under composition and inversion, so $F \supseteq S$ is all that is available; whether the inclusion is an equality is not part of what is being said here.

Throughout the statement, $F$ is treated as a group in its own right: its elements are the elements of $G$ that lie in $F$, and its multiplication, identity and inversion are those of $G$ restricted to $F$.

The abelianization $F^{\mathrm{ab}}$

Let $[F,F]$ denote the commutator subgroup of $F$: the subgroup of $F$ generated by all commutators

$$g h g^{-1} h^{-1}, \qquad g, h \in F,$$

that is, the smallest subgroup of $F$ containing every such element. (Commutators are formed inside $F$, with both entries ranging over all of $F$.)

Then

$$F^{\mathrm{ab}} \;=\; F \big/ [F,F],$$

the quotient of $F$ by that subgroup, taken as the set of equivalence classes under

$$g \sim h \iff g^{-1}h \in [F,F],$$

carrying the multiplication induced from $F$. This is a group, and an abelian one. In the statement it is this quotient group that appears on the left-hand side.

The target group

The right-hand side is the set $\mathbb{Z} \times \mathbb{Z}$ of ordered pairs of integers, carrying the operation

$$(a,b) \cdot (c,d) \;=\; (a + c,\ b + d),$$

i.e. componentwise integer addition, written multiplicatively. The underlying set is literally the set of integer pairs; only the name and symbol of the operation change. This is the free abelian group of rank two, with its two additive coordinates.

Two readings that are not intended, and are excluded by what is written: the target is not a direct product of two copies of some separate multiplicative group, and the operation is not componentwise multiplication of integers. It is componentwise addition, relabelled.

The isomorphism that is claimed to exist

The objects whose existence is asserted are multiplication-preserving equivalences. Such an object consists of exactly the following data and properties:

• a map $\varphi : F^{\mathrm{ab}} \to \mathbb{Z} \times \mathbb{Z}$;
• a map $\psi : \mathbb{Z} \times \mathbb{Z} \to F^{\mathrm{ab}}$;
• the identity $\psi(\varphi(u)) = u$ for every $u \in F^{\mathrm{ab}}$;
• the identity $\varphi(\psi(v)) = v$ for every $v \in \mathbb{Z} \times \mathbb{Z}$;
• multiplicativity: $\varphi(u_1 u_2) = \varphi(u_1)\,\varphi(u_2)$ for all $u_1, u_2 \in F^{\mathrm{ab}}$ — spelled out with the operations above, this says

$$\varphi(u_1 u_2) \;=\; \varphi(u_1) + \varphi(u_2)$$

in $\mathbb{Z} \times \mathbb{Z}$, coordinatewise.

The two round-trip identities make $\varphi$ a bijection with $\psi$ as its inverse. Note that preservation of the identity element and of inverses is not among the demands: the required data is a bijection together with multiplicativity, nothing more. (For groups these further properties follow, but they are not what is being asserted.)

Finally, the statement asserts the nonemptiness of the collection of such objects, as a proposition. It does not name, construct or characterise one; it does not claim that any two of them agree; and it carries no information about which isomorphism, among possibly many, one might obtain.

Degenerate and edge cases

• There are no hypotheses in this statement, hence none that could be vacuous or impossible to satisfy. Nothing needs to be supplied to instantiate it.
• $k = 0$ is allowed in the definition of dyadic, so every integer is dyadic.
• $B = \varnothing$ is allowed in the generating condition, as noted above.
• The generating condition places no requirement on $f$ at a single point in isolation: its hypothesis requires $x < y$ strictly, so degenerate intervals impose nothing directly.
• Because the target is $\mathbb{Z} \times \mathbb{Z}$ and not merely "some abelian group", the statement carries quantitative content about $F^{\mathrm{ab}}$: it says $F^{\mathrm{ab}}$ is infinite, torsion-free, and generated by exactly two independent elements. It is strictly stronger than saying that $F^{\mathrm{ab}}$ is abelian, or finitely generated, or free abelian of some unspecified rank.