Read-back: isSimpleGroup_commutator

The declaration is a closed proposition: it has no variables, no hypotheses, and no typeclass assumptions of its own. Everything quantified sits inside the definitions it invokes, and those are expanded in full below.

In one sentence, it asserts:

The commutator subgroup of the group $F$ — where $F$ is the group generated by the piecewise-linear, dyadic-breakpoint, power-of-two-slope order isomorphisms of $[0,1]$ — is a simple group.

The rest of this note unfolds every phrase of that sentence.

---

1. The unit interval as a type, and its order isomorphisms

Let

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

regarded as a set of reals carrying the order it inherits from $\mathbb{R}$. (Its elements are reals together with a proof of membership; two elements are equal exactly when the underlying reals are equal.)

An order isomorphism of $I$ is a pair of mutually inverse maps $f : I \to I$ and $f^{-1} : I \to I$ (so $f^{-1}(f(x)) = x$ and $f(f^{-1}(x)) = x$ for all $x \in I$) subject to

$$f(x) \le f(y) \iff x \le y \qquad \text{for all } x,y \in I .$$

No continuity, and no topology of any kind, is required of $f$. An order isomorphism is an order-theoretic object only; that it happens to be continuous is not part of the data or of the requirements.

Write

$$G := \{\text{order isomorphisms of } I\}.$$

$G$ is a group. Its multiplication is composition of maps in the usual right-to-left reading:

$$(f \cdot g)(x) = f(g(x)),$$

its identity element is the identity map of $I$, and the inverse of $f$ in the group is the inverse map $f^{-1}$. This direction matters for everything below, and it is the ordinary composition convention.

2. Dyadic rationals

A real number $x$ is called dyadic when

$$\exists\, m \in \mathbb{Z},\ \exists\, k \in \mathbb{N} : \quad x = \frac{m}{2^{k}} .$$

Here $k$ ranges over the natural numbers including $0$, and $m$ over all integers, positive, negative and zero. So every integer is dyadic, and the dyadic numbers form the usual set $\mathbb{Z}[1/2]$. No restriction confines them to $[0,1]$.

3. The generating condition

An order isomorphism $f \in G$ is said to satisfy the Thompson condition when:

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

1. every element of $B$ is dyadic, and
2. for every pair $x, y \in I$ with $x < y$ such that the open interval $(x,y)$ is disjoint from $B$, i.e. $(x,y) \cap B = \varnothing$, there exist an integer $n \in \mathbb{Z}$ and a real $c \in \mathbb{R}$ with

$$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 stating explicitly, because the quantifiers silently allow them:

• The exponent $n$ is an arbitrary integer, so the permitted slopes are exactly the numbers $2^{n}$ for $n \in \mathbb{Z}$: all positive, and allowed to be less than $1$ (e.g. $1/2$, $1/4$) as well as greater.
• The intercept $c$ is an arbitrary real number. It is not required to be dyadic, and nothing in this statement asserts that it must be.
• The exclusion condition is on the open interval $(x,y)$, whereas the affine formula is demanded on the closed interval $[x,y]$. So the endpoints $x$ and $y$ are themselves permitted to lie in $B$, and the affine formula is nonetheless required to hold at them.
• $n$ and $c$ are chosen after $x$ and $y$: different admissible pairs $(x,y)$ may get different slopes and intercepts.
• $B$ is only required to be some finite set of dyadic reals off which $f$ is affine. It is not asserted to be the set of actual breakpoints of $f$, it may be larger than that set, it may contain points lying outside $[0,1]$, and it is permitted to be empty — in which case clause 2 applies to every pair $x<y$ in $I$ and demands a single affine formula on all of $I$.
• The quantifiers $x, y$ range over $I$, so only pairs of points of $[0,1]$ are tested.

Write

$$S := \{f \in G : f \text{ satisfies the Thompson condition}\}.$$

4. The group $F$

$$F := \text{the subgroup of } G \text{ generated by } S,$$

that is, 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 $f_1^{\pm 1} f_2^{\pm 1} \cdots f_r^{\pm 1}$ with each $f_i \in S$ (the empty product being the identity).

$F$ is the generated subgroup, not the set $S$ itself. Nothing in this declaration asserts that $S$ is already closed under composition and inversion, so nothing here says $F = S$; a priori $F$ may be strictly larger than $S$.

$F$ is then regarded as a group in its own right: its elements are the elements of $G$ lying in $F$, and its multiplication, identity and inversion are those of $G$ restricted to $F$.

5. The commutator subgroup of $F$

For $g_1, g_2$ in a group, the commutator is taken in the convention

$$[g_1, g_2] := g_1\, g_2\, g_1^{-1}\, g_2^{-1}.$$

(With the composition convention of §1, this is the map $g_1 \circ g_2 \circ g_1^{-1} \circ g_2^{-1}$.)

The commutator subgroup of $F$ is

$$K := \langle\, [g_1,g_2] \;:\; g_1, g_2 \in F \,\rangle,$$

the subgroup of $F$ generated by all commutators of pairs of elements of $F$. This is the smallest subgroup of $F$ containing every such commutator; it is not merely the set of commutators, which need not be a subgroup.

Two points of placement:

• $K$ is a subgroup of $F$, and the commutators are formed from elements of $F$ using the group operations of $F$ — not from arbitrary elements of the ambient group $G$.
• $K$ is likewise then regarded as a group in its own right, with the operations inherited from $F$.

6. The assertion

The declaration asserts that $K$ is a simple group. Unfolded, this is the conjunction of two claims:

(a) Nontriviality. There exist elements $u, v \in K$ with $u \ne v$; equivalently, $K$ has more than one element, i.e. $K \ne \{1\}$.

(b) Every normal subgroup is trivial or everything. For every subgroup $H \le K$, if $H$ is normal in $K$ — meaning

$$\forall\, h \in H,\ \forall\, g \in K : \quad g\,h\,g^{-1} \in H$$

— then

$$H = \{1\} \quad\text{or}\quad H = K .$$

Here $\{1\}$ is the subgroup of $K$ whose only element is the identity, and $K$ denotes the subgroup of $K$ consisting of all of $K$; the disjunction is an inclusive "or", and the equality is equality of subgroups (equivalently, of their underlying sets).

Note that nontriviality is genuinely part of the claim, not a side condition: the trivial group would satisfy (b) vacuously, and (a) is what excludes it.

Note also that normality in (b) is normality inside $K$, with the conjugating element $g$ ranging over $K$ only — not over $F$, and not over $G$.