Commuting elements of a free group

An abelian subgroup of a free group is cyclic. This gives an intrinsic characterization of commuting pairs: they are integer powers of a common element. The argument uses the Nielsen–Schreier theorem and the fact that a free group on two distinct generators is not abelian. It applies without choosing reduced-word representatives or a finite basis.

theorem IsFreeGroup.isCyclic_of_isMulCommutative {G : Type u_1} [Group G] [IsFreeGroup G] [IsMulCommutative G] : IsCyclic G

A commutative free group is cyclic.

theorem Subgroup.isCyclic_of_isMulCommutative {G : Type u_1} [Group G] [IsFreeGroup G] (H : Subgroup G) [IsMulCommutative ↥H] : IsCyclic ↥H

Every abelian subgroup of a free group is cyclic, including the trivial subgroup.

theorem IsFreeGroup.commute_iff_exists_common_zpow {G : Type u_1} [Group G] [IsFreeGroup G] (x y : G) : Commute x y ↔ ∃ (r : G) (m : ℤ) (n : ℤ), x = r ^ m ∧ y = r ^ n

Two elements of a free group commute exactly when they are integer powers of one element.