A free group is nilpotent exactly in rank at most one

Let x and y be two distinct generators of the free group FreeGroup X. The left-normed commutators

w_0 = x, w_{n+1} = ⁅w_n, y⁆

satisfy w_n ∈ γ_n, the n-th term of the lower central series, and none of them is trivial. Hence no term of the lower central series of a free group of rank at least two is trivial, and such a free group is not nilpotent. Conversely, a free group of rank at most one is cyclic, hence nilpotent.

The nontriviality is detected in the infinite dihedral group DihedralGroup 0, the group of isometries t ↦ ±t + m of ℤ. Send x to the translation r 1 : t ↦ t + 1 and every other generator to the reflection sr 0 : t ↦ -t. The commutator of a translation r m with the reflection is the translation r (2 * m), so w_n maps to the translation r (2 ^ n), which is not the identity.

Main results

• FreeGroup.iterate_commutatorElement_ne_one: the left-normed commutator ⁅⋯⁅⁅x, y⁆, y⁆, ⋯, y⁆ of two distinct generators is nontrivial.
• FreeGroup.lowerCentralSeries_ne_bot: no term of the lower central series of a free group of rank at least two is trivial.
• FreeGroup.isNilpotent_iff_subsingleton: a free group is nilpotent if and only if it has at most one generator.

References

• W. Magnus, A. Karrass and D. Solitar, Combinatorial Group Theory, Chapter 5, for the lower central series of free groups.

theorem FreeGroup.iterate_commutatorElement_ne_one {X : Type u_1} {i j : X} (hij : i ≠ j) (n : ℕ) : (fun (w : FreeGroup X) => ⁅w, of j⁆)^[n] (of i) ≠ 1

Left-normed commutators of two generators are nontrivial. For distinct generators x_i and x_j of a free group, the iterated commutator ⁅⋯⁅⁅x_i, x_j⁆, x_j⁆, ⋯, x_j⁆ with n brackets is not the identity.

theorem FreeGroup.lowerCentralSeries_ne_bot {X : Type u_1} [Nontrivial X] (n : ℕ) : ⊤.lowerCentralSeries n ≠ ⊥

The lower central series of a free group of rank at least two never vanishes. Every term γ_n contains the nontrivial left-normed commutator ⁅⋯⁅⁅x_i, x_j⁆, x_j⁆, ⋯, x_j⁆ of two distinct generators.

@[simp]

theorem FreeGroup.isNilpotent_iff_subsingleton {X : Type u_1} : Group.IsNilpotent (FreeGroup X) ↔ Subsingleton X

A free group is nilpotent if and only if it has at most one generator.