Centralizers in free groups

A free group on at least two generators has trivial centre. Consequently, a free group with a nontrivial central element is commutative, and, since subgroups of free groups are free (Nielsen–Schreier), commutation is transitive on the nontrivial elements of a free group. The centralizer of a nontrivial element of a free group is therefore abelian, hence cyclic.

These are the facts from which maximal roots of elements of a free group are built, in TauCeti.GroupTheory.FreeGroup.MaximalRoot.Basic. Free groups are also shown to have unique roots for a fixed nonzero exponent, transporting Mathlib's instance for FreeGroup α along a free basis.

Main results

• FreeGroup.mem_zpowers_of_of_commute: an element commuting with a generator of a is a power of of a.
• FreeGroup.center_eq_bot_of_nontrivial: the centre of a free group on at least two generators is trivial.
• IsFreeGroup.commute_of_commute: in a free group, two elements commuting with a common nontrivial element commute with each other.
• IsFreeGroup.isCyclic_centralizer: the centralizer of a nontrivial element of a free group is cyclic.

References

• G. Baumslag, A. Myasnikov, V. Remeslennikov, Algebraic geometry over groups I. Algebraic sets and ideal theory, J. Algebra 219 (1999), §2.1 (free groups are commutative transitive).
• 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 (centralizers of nontrivial elements of a free group are cyclic).

theorem FreeGroup.mem_zpowers_of_of_commute {α : Type u_1} {a : α} {z : FreeGroup α} (h : Commute z (of a)) : z ∈ Subgroup.zpowers (of a)

An element of a free group commuting with a generator of a is a power of of a.

theorem FreeGroup.center_eq_bot_of_nontrivial {α : Type u_1} [Nontrivial α] : Subgroup.center (FreeGroup α) = ⊥

The centre of a free group on at least two generators is trivial.

instance IsFreeGroup.instHasUniqueRoots_tauCeti {G : Type u_1} [Group G] [IsFreeGroup G] : HasUniqueRoots G

A free group has unique roots for every fixed nonzero exponent: x ^ n = y ^ n with n ≠ 0 forces x = y. In particular a free group is torsion-free.

theorem IsFreeGroup.isMulCommutative_of_mem_center {G : Type u_1} [Group G] [IsFreeGroup G] {x : G} (hx : x ∈ Subgroup.center G) (hx1 : x ≠ 1) : IsMulCommutative G

A free group with a nontrivial central element is commutative.

theorem IsFreeGroup.commute_of_commute {G : Type u_1} [Group G] [IsFreeGroup G] {x y z : G} (hy : y ≠ 1) (hxy : Commute x y) (hyz : Commute y z) : Commute x z

Commutation is transitive on the nontrivial elements of a free group: if x and z both commute with a nontrivial element y, then x and z commute.

theorem IsFreeGroup.isMulCommutative_centralizer {G : Type u_1} [Group G] [IsFreeGroup G] {x : G} (hx : x ≠ 1) : IsMulCommutative ↥(Subgroup.centralizer {x})

The centralizer of a nontrivial element of a free group is abelian.

theorem IsFreeGroup.isCyclic_centralizer {G : Type u_1} [Group G] [IsFreeGroup G] {x : G} (hx : x ≠ 1) : IsCyclic ↥(Subgroup.centralizer {x})

The centralizer of a nontrivial element of a free group is cyclic.