Read-back: mul_comm_quotient_of_ne_bot

Summary of the assertion

The declaration asserts: for every normal subgroup $N$ of the group $F$ defined below, if $N$ is not the trivial subgroup, then any two elements of the quotient group $F/N$ commute.

Everything in that sentence — what $F$ is, what its group law is, what "normal", "trivial" and "quotient" mean here — is spelled out below, because $F$ is built from definitions supplied with the statement rather than taken from a standard library.

The ambient group

Let

$$I = [0,1] = \{t \in \mathbb{R} : 0 \le t \le 1\},$$

regarded as an ordered set with the order it inherits from $\mathbb{R}$ (one element of $I$ is $\le$ another exactly when the corresponding real numbers are).

Let $\operatorname{Aut}(I)$ denote the set of order isomorphisms of $I$ onto itself: each such object is a bijection $f : I \to I$ together with the property that for all $a,b \in I$,

$$a \le b \iff f(a) \le f(b).$$

(Formally it is an equivalence of $I$ with itself carrying that order-reflecting property; no continuity, differentiability or topological condition is imposed, and none is available for free from this data.)

$\operatorname{Aut}(I)$ is a group under composition of maps, with

$$(g \cdot h)(t) = g\bigl(h(t)\bigr)$$

for all $t \in I$, identity element the identity map of $I$, and inverse the inverse order isomorphism. So the product is read right-to-left in the usual functional way: in $g \cdot h$, the map $h$ acts first.

Dyadic rationals

A real number $x$ is called dyadic here if there exist an integer $m \in \mathbb{Z}$ and a natural number $k \in \mathbb{N}$ (with $0$ allowed) such that

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

Note that this admits negative and arbitrarily large dyadics, and every integer ($k = 0$); it is not restricted to $[0,1]$.

The generating condition

Call $f \in \operatorname{Aut}(I)$ Thompson-like if there exists a finite set $B \subseteq \mathbb{R}$ of real numbers such that

1. every $b \in B$ is dyadic in the sense above, and
2. for all $x, y \in I$ with $x < y$ (as real numbers) such that the open real interval $(x,y)$ contains no element of $B$, 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 are worth making explicit, since they are what the statement actually carries:

• The finite set $B$ is chosen once, before the pair $x,y$: a single finite breakpoint set must work for all admissible pairs. The exponent $n$ and the intercept $c$, by contrast, are chosen after $x,y$ and may vary with the pair.
• $B$ is an arbitrary finite set of dyadic reals. It is not required to be contained in $[0,1]$, not required to consist of actual points of non-differentiability, and it may be empty — in which case condition 2 applies to every pair $x < y$ in $I$ and forces a single affine formula on all of $I$.
• The slope is $2^{n}$ with $n$ ranging over all integers, so slopes are the positive integer powers of $2$ and their reciprocals; $2^{n}$ is in particular always strictly positive, and never $0$.
• The intercept $c$ is an unconstrained real number: it is not required to be dyadic.
• The affine identity is required on the closed interval $x \le z \le y$, so it pins the formula down at the two endpoints as well as strictly between them.
• Condition 2 is a condition on $f$ only; nothing is said about $f^{-1}$, and nothing beyond order-isomorphy is asserted about $f$ at the endpoints $0$ and $1$.

The group $F$

Let $S = \{ f \in \operatorname{Aut}(I) : f \text{ is Thompson-like} \}$, and define

$$F = \langle S \rangle,$$

the subgroup of $\operatorname{Aut}(I)$ generated by $S$: the intersection of all subgroups of $\operatorname{Aut}(I)$ containing $S$, equivalently the set of all finite products of elements of $S$ and their inverses.

This is a generated subgroup, not the set $S$ itself. The statement does not assert, use, or presuppose that $S$ is already closed under composition and inversion; $F$ may a priori be strictly larger than $S$.

In the statement, $F$ is used as a group in its own right: its elements are the order isomorphisms of $I$ belonging to $F$, its multiplication is composition as above, and its identity is the identity map of $I$.

The hypotheses

Let $N$ be a subgroup of $F$ — a subgroup of $F$ itself, not of the larger group $\operatorname{Aut}(I)$: a subset of $F$ containing the identity map and closed under composition and inversion.

Two hypotheses are imposed on $N$:

1. $N$ is normal in $F$: for every $n \in N$ and every $g \in F$, one has $g n g^{-1} \in N$. Normality is relative to $F$ alone; nothing is required about conjugation by elements of $\operatorname{Aut}(I)$ outside $F$.
2. $N$ is not the trivial subgroup: $N \ne \{\mathrm{id}_I\}$. Equivalently, $N$ contains at least one element other than the identity map of $I$.

Both are genuine hypotheses of the assertion; the first is supplied as a structural (typeclass) assumption and the second as an explicit one, but logically they play the same role.

Note what is not assumed: $N$ is not required to be a proper subgroup. The case $N = F$ is included, and in that case $F/N$ is the one-element group.

The conclusion

Under those hypotheses, form the quotient group $F/N$. Its elements are the left cosets

$$xN = \{xn : n \in N\}, \qquad x \in F,$$

two elements $x, y \in F$ determining the same coset exactly when $x^{-1}y \in N$; its group law is the well-defined one induced by that of $F$,

$$(xN)\,(yN) = (xy)N,$$

which is where normality of $N$ is needed.

The conclusion asserted is:

$$\forall\, \xi, \eta \in F/N : \quad \xi \eta = \eta \xi .$$

That is, the quotient group $F/N$ is abelian. The two quotient elements $\xi,\eta$ are universally quantified, so the assertion is exactly the commutativity of $F/N$, stated element-wise rather than as a structure on the quotient.

Scope and degenerate cases

• The statement is a single implication, quantified over all normal $N \ne \{\mathrm{id}_I\}$ and all pairs of elements of $F/N$. It is not an equivalence: nothing is asserted in the direction "if $F/N$ is abelian then $N \ne \{\mathrm{id}_I\}$".
• Nothing is asserted about $F/\{\mathrm{id}_I\} \cong F$ itself; the excluded case $N = \{\mathrm{id}_I\}$ is precisely the one for which no claim is made.
• Nothing is asserted about how large $F/N$ is, about the structure of $N$, or about whether any $N$ satisfying the hypotheses exists.
• Possible vacuity. The hypotheses can be satisfied only if $F$ contains some element other than the identity map (otherwise every subgroup of $F$ is the trivial one and the hypothesis $N \ne \{\mathrm{id}_I\}$ is unsatisfiable). The definitions supplied alongside the statement construct two candidate maps of $I$ but do not themselves record that either one lies in $F$, nor that $F$ is nontrivial. So non-vacuity is not something the accompanying material establishes; it is an external fact about the definition of $F$.
• The definition of $F$ quantifies over all Thompson-like maps as generators, so the group is fixed by the definitions above and carries no further parameters: the statement has no free variables beyond $N$, the normality assumption, and the two quotient elements.