The ping-pong lemma for cyclic subgroups

Mathlib's free-group ping-pong lemma FreeGroup.injective_lift_of_ping_pong asks for two sets X i and Y i per generator, with a i mapping the complement of Y i into X i and (a i)⁻¹ mapping the complement of X i into Y i. In the classical cyclic form (de la Harpe, Topics in geometric group theory, §II.B) there is one set X i per generator, and every nonzero power of a i maps every other X j into X i. This form is the one that applies directly to the matrices [[1, 2], [0, 1]] and [[1, 0], [2, 1]] acting on ℤ². It is deduced here from Mathlib's ping-pong lemma for free products, Monoid.CoprodI.lift_injective_of_ping_pong, through freeGroupEquivCoprodI, following Mathlib's own proof of FreeGroup.injective_lift_of_ping_pong.

A second statement turns one ping-pong pair into infinitely many: if a and b play ping-pong on two disjoint sets, then the conjugates bᵏ a b⁻ᵏ, for distinct integers k, freely generate a free group. This is how free groups of every countable rank are found inside a free group of rank two, and inside SL(2, ℤ).

Main results

• FreeGroup.injective_lift_of_ping_pong_zpow: the cyclic ping-pong lemma.
• FreeGroup.injective_lift_of_ping_pong_pair: its two-generator form.
• FreeGroup.injective_lift_conj_zpow_of_ping_pong: conjugates of a ping-pong partner by distinct powers of the other one are a free basis of the subgroup they generate.

References

• P. de la Harpe, Topics in geometric group theory, University of Chicago Press, 2000, §II.B (the table-tennis lemma).

theorem FreeGroup.injective_lift_of_ping_pong_zpow {ι : Type u_1} {G : Type u_2} {α : Type u_3} [Group G] [MulAction G α] [Nontrivial ι] (a : ι → G) (X : ι → Set α) (hX : ∀ (i : ι), (X i).Nonempty) (hXdisj : Pairwise (Function.onFun Disjoint X)) (hpp : Pairwise fun (i j : ι) => ∀ (n : ℤ), n ≠ 0 → a i ^ n • X j ⊆ X i) : Function.Injective ⇑(lift a)

The ping-pong lemma, cyclic form. Suppose there are at least two indices. If every nonzero power of a i maps every set X j with j ≠ i into X i, where the sets X i are nonempty and pairwise disjoint, then the a i freely generate a free subgroup: FreeGroup.lift a is injective.

theorem FreeGroup.injective_lift_of_ping_pong_pair {G : Type u_2} {α : Type u_3} [Group G] [MulAction G α] {a b : G} {X Y : Set α} (hX : X.Nonempty) (hXY : Disjoint X Y) (ha : ∀ (n : ℤ), n ≠ 0 → a ^ n • Y ⊆ X) (hb : ∀ (n : ℤ), n ≠ 0 → b ^ n • X ⊆ Y) : Function.Injective ⇑(lift ![a, b])

The ping-pong lemma for two elements. If every nonzero power of a maps Y into X, and every nonzero power of b maps X into Y, where X is nonempty and X and Y are disjoint, then a and b freely generate a free group of rank two.

theorem FreeGroup.injective_lift_conj_zpow_of_ping_pong {ι : Type u_1} {G : Type u_2} {α : Type u_3} [Group G] [MulAction G α] {a b : G} {X Y : Set α} (hX : X.Nonempty) (hXY : Disjoint X Y) (ha : ∀ (n : ℤ), n ≠ 0 → a ^ n • Y ⊆ X) (hb : ∀ (n : ℤ), n ≠ 0 → b ^ n • X ⊆ Y) {k : ι → ℤ} (hk : Function.Injective k) : Function.Injective ⇑(lift fun (i : ι) => b ^ k i * a * (b ^ k i)⁻¹)

Free subgroups from conjugates. Let a and b play ping-pong on disjoint sets X and Y with X nonempty: every nonzero power of a maps Y into X, and every nonzero power of b maps X into Y. Then for an injective family of exponents k : ι → ℤ, the conjugates b ^ k i * a * (b ^ k i)⁻¹ freely generate a free subgroup.