Maximal roots in free groups

Every nontrivial element x of a free group is a positive power r ^ k of exactly one element r that is not a proper power; r is the maximal root of x. The centralizer of x is the cyclic group generated by r, and the positive-exponent roots of x are exactly the powers r ^ (k / n) with n ∣ k.

The identity is excluded: it is itself a proper power (1 = 1 ^ 2), so it has no maximal root, and its centralizer is the whole group.

The results hold for every group with IsFreeGroup, in particular for FreeGroup α.

Conjugation and inversion transport maximal roots: (g * r * g⁻¹) ^ k = g * x * g⁻¹ and r⁻¹ ^ k = x⁻¹, and neither operation creates or destroys proper powers (Group.isProperPower_conj_iff, Group.isProperPower_inv), so by uniqueness the maximal roots of g * x * g⁻¹ and x⁻¹ are g * r * g⁻¹ and r⁻¹, with the same exponent.

Main results

• IsFreeGroup.exists_maximalRoot: a nontrivial element of a free group is r ^ k for a unique pair (r, k) with k ≠ 0 and r not a proper power.

• IsFreeGroup.pow_eq_pow_iff_of_not_isProperPower: for non-proper-powers r, s and nonzero exponents, r ^ k = s ^ l ↔ r = s ∧ k = l.

• IsFreeGroup.pow_eq_iff_dvd_and_eq_pow_div: if r ^ k = x is the maximal root decomposition, then y ^ n = x ↔ n ∣ k ∧ y = r ^ (k / n) for n ≠ 0.

• IsFreeGroup.centralizer_singleton_eq_zpowers: the centralizer of x is generated by its maximal root.

• IsFreeGroup.centralizer_singleton_eq_zpowers_self: the centralizer of a non-proper-power u is zpowers u.

• Group.maximalRoot_conj, Group.maximalRoot_inv, Group.maximalRoot_pow: transport maximal-root decompositions under conjugation, inversion, and positive powers.

References

• O. Kharlampovich, A. Myasnikov, V. Remeslennikov, D. Serbin, Subgroups of fully residually free groups: algorithmic problems, Contemp. Math. 360 (2004), §5, proof of Lemma 21 (maximal roots, and centralizers of nontrivial elements of a free group).

theorem IsFreeGroup.centralizer_singleton_eq_zpowers {G : Type u_1} [Group G] [IsFreeGroup G] {x r : G} {k : ℕ} (hk : k ≠ 0) (hr : ¬Group.IsProperPower r) (hx : r ^ k = x) : Subgroup.centralizer {x} = Subgroup.zpowers r

In a free group, the centralizer of r ^ k, for k ≠ 0 and r not a proper power, is the cyclic group generated by r.

theorem IsFreeGroup.centralizer_singleton_eq_zpowers_self {G : Type u_1} [Group G] [IsFreeGroup G] {u : G} (hu : ¬Group.IsProperPower u) : Subgroup.centralizer {u} = Subgroup.zpowers u

In a free group, the centralizer of an element u that is not a proper power is the cyclic group generated by u.

theorem IsFreeGroup.pow_eq_pow_iff_of_not_isProperPower {G : Type u_1} [Group G] [IsFreeGroup G] {r s : G} {k l : ℕ} (hk : k ≠ 0) (hl : l ≠ 0) (hr : ¬Group.IsProperPower r) (hs : ¬Group.IsProperPower s) : r ^ k = s ^ l ↔ r = s ∧ k = l

Uniqueness of maximal roots in a free group: if r and s are not proper powers and the exponents k, l are nonzero, then r ^ k = s ^ l exactly when r = s and k = l.

theorem IsFreeGroup.exists_maximalRoot {G : Type u_1} [Group G] [IsFreeGroup G] {x : G} (hx : x ≠ 1) : ∃! p : G × ℕ, p.2 ≠ 0 ∧ p.1 ^ p.2 = x ∧ ¬Group.IsProperPower p.1

Maximal roots in a free group. Every nontrivial element x of a free group is r ^ k for a unique pair (r, k) with k ≠ 0 and r not a proper power.

theorem IsFreeGroup.pow_eq_iff_dvd_and_eq_pow_div {G : Type u_1} [Group G] [IsFreeGroup G] {x r y : G} {k n : ℕ} (hk : k ≠ 0) (hr : ¬Group.IsProperPower r) (hx : r ^ k = x) (hn : n ≠ 0) : y ^ n = x ↔ n ∣ k ∧ y = r ^ (k / n)

The positive-exponent roots of an element of a free group are powers of its maximal root: if r ^ k = x with k ≠ 0 and r not a proper power, then for n ≠ 0, y ^ n = x exactly when n ∣ k and y = r ^ (k / n).