Read-back: no_free_subgroup_of_rank_two

The ambient group

Let $I = [0,1] = \{x \in \mathbb{R} : 0 \le x \le 1\}$, regarded as a set of real numbers and carrying the order it inherits from $\mathbb{R}$: for $a, b \in I$, $a \le b$ means exactly $a \le b$ as real numbers.

Let

$$G = \operatorname{Aut}_{\le}(I)$$

be the collection of order isomorphisms of $I$: bijections $u : I \to I$ such that for all $a, b \in I$,

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

(Equivalently, order-preserving bijections whose inverse is also order-preserving. No continuity, differentiability or piecewise structure is part of this datum; the objects carry an order-theoretic structure only.)

$G$ is a group under composition, with

• product: $(u \cdot v)(x) = u\bigl(v(x)\bigr)$ — so in a product the right-hand factor acts first;
• identity element: the identity map of $I$;
• inverse of $u$: the inverse bijection $u^{-1}$.

Three definitions the statement uses

Dyadic. A real number $x$ is called dyadic when

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

with $\mathbb{N}$ including $0$ (so every integer is dyadic) and the quotient taken in $\mathbb{R}$.

The generating condition. For $u \in G$, say that $u$ satisfies the piecewise-linearity 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$ whose open interval misses $B$, that is

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

there exist an integer $n \in \mathbb{Z}$ and a real number $c \in \mathbb{R}$ such that

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

Points to note about this condition, since they are what the quantifiers literally say:

• $B$ is an arbitrary finite set of real numbers. It is not required to be non-empty, not required to lie inside $[0,1]$, and it is not required to consist of actual breakpoints of $u$ — it is merely a finite dyadic set outside which $u$ is affine in the stated sense.
• The interval that must avoid $B$ is the open interval $(x,y)$, whereas the affine formula is demanded on the closed interval $[x,y]$ — so the formula is pinned down at the endpoints $x$ and $y$ as well, and the endpoints themselves are allowed to lie in $B$.
• The exponent $n$ ranges over all integers, so the slope $2^n$ is any positive integer power of $2$, negative exponents included. The intercept $c$ is an unconstrained real number — nothing here requires it to be dyadic.
• $n$ and $c$ are chosen after $x$ and $y$: they may depend on the pair $(x,y)$.
• Nothing is required of $u$ on a pair $x<y$ whose open interval does meet $B$.

The group $F$. Let $S = \{u \in G : u \text{ satisfies the piecewise-linearity condition}\}$ and let

$$F = \langle S \rangle \le G$$

be the subgroup of $G$ generated by $S$ — by definition the intersection of all subgroups of $G$ that contain $S$, equivalently the set of all finite products of elements of $S$ and inverses of elements of $S$ (the empty product giving the identity).

Note that $F$ is defined as this generated subgroup, not as $S$ itself. The statement does not assume, and nothing above asserts, that $S$ is already closed under composition and inverses; membership $u \in F$ is therefore a strictly weaker hypothesis on the face of it than "$u$ satisfies the piecewise-linearity condition".

The free group and the comparison map

Let $F_2$ denote the free group on a two-element index set $\{0, 1\}$: formally, the set of finite words in the letters $0, 1$ and their formal inverses, taken modulo free cancellation (deleting an adjacent pair $x\,x^{-1}$ or $x^{-1}x$), with concatenation as multiplication, the empty word as identity, and reversal-with-inversion as inverse. The two generators $x_0, x_1$ are distinct elements of $F_2$, so this really is the free group of rank two.

Given any two elements $f, g \in G$ there is a unique group homomorphism

$$\varphi_{f,g} : F_2 \longrightarrow G, \qquad \varphi_{f,g}(x_0) = f, \quad \varphi_{f,g}(x_1) = g .$$

Concretely, a word

$$w = x_{i_1}^{e_1} x_{i_2}^{e_2} \cdots x_{i_k}^{e_k}, \qquad i_j \in \{0,1\},\ e_j = \pm 1,$$

is sent to the composite

$$\varphi_{f,g}(w) = h_{i_1}^{e_1} \circ h_{i_2}^{e_2} \circ \cdots \circ h_{i_k}^{e_k}, \qquad h_0 = f,\ h_1 = g,$$

read with the last letter of the word applied to the point first. The empty word is sent to the identity map. (Which of the two generators goes to $f$ and which to $g$ is fixed as above, but is immaterial to the assertion below.)

What the declaration asserts

For every order isomorphism $f$ of $[0,1]$, for every order isomorphism $g$ of $[0,1]$, if $f \in F$ and $g \in F$, then the homomorphism $\varphi_{f,g} : F_2 \to G$ is not injective.

Injectivity here is the ordinary notion for the underlying map of sets: $\varphi_{f,g}$ is injective when for all $u, v \in F_2$, $\varphi_{f,g}(u) = \varphi_{f,g}(v)$ implies $u = v$. The declaration asserts the negation of that, for every admissible $f$ and $g$. Spelled out, the conclusion says:

$$\exists\, u, v \in F_2 \ \text{ with } \ u \neq v \ \text{ and } \ \varphi_{f,g}(u) = \varphi_{f,g}(v),$$

or equivalently (translating by $u v^{-1}$):

$$\exists\, w \in F_2 \ \text{ with } \ w \neq 1 \ \text{ and } \ \varphi_{f,g}(w) = \mathrm{id}_{[0,1]} ,$$

i.e. the pair $(f,g)$ satisfies some non-trivial relation as a word in $f$, $g$ and their inverses.

Binders and hypotheses, in full

There are exactly four binders, all of them explicit arguments:

1. $f$, an order isomorphism of $[0,1]$;
2. $g$, an order isomorphism of $[0,1]$;
3. a hypothesis $f \in F$;
4. a hypothesis $g \in F$.

There are no further quantified variables, no implicit arguments, and no structural or typeclass assumptions carried as hypotheses: the order on $[0,1]$ used throughout is the one inherited from the real numbers, and the group structure on $G$ is the composition structure described above; both are fixed, not quantified over.

Degenerate and edge cases included

• The hypotheses are satisfiable, and the statement is not vacuous. $F$ is a subgroup, so it contains the identity map of $[0,1]$; taking $f = g = \mathrm{id}$ satisfies both hypotheses. The statement therefore does assert something about at least one pair.
• $f$ and $g$ are not required to be distinct. The case $f = g$ is included, as are the cases where one or both of $f, g$ is the identity map, and the case where $f$ and $g$ commute or where one is a power of the other. The assertion is made uniformly for all such pairs.
• No constraint ties $f$ and $g$ to each other or to $F$'s generators. They need not generate $F$, need not generate a proper subgroup, need not satisfy the piecewise-linearity condition themselves (only membership in the generated subgroup $F$ is assumed), and need not have any prescribed fixed points or supports.
• The rank is exactly two. The index set of the free group is a two-element set; the assertion concerns the free group on two generators and no other rank.
• Injectivity is on all of $F_2$. The failure of injectivity asserted is failure on the whole free group of rank two, which is the same as: the map is non-injective somewhere. It is not a claim that the map has some prescribed kernel, nor a claim about any particular word.