Conjugacy and cyclic rotation in free groups

Rotating a word conjugates the free-group element it represents. Together with Mathlib's explicit cyclic-reduction conjugator, this relates rotation of cyclic reductions to conjugacy of the original elements.

Conversely, two cyclically reduced words represent conjugate elements only if they are rotations of each other. This gives the classical conjugacy criterion in free groups: x and y are conjugate exactly when the cyclic reductions of their reduced words are cyclic rotations of each other.

Main results

• FreeGroup.IsCyclicallyReduced.rotate: rotations of cyclically reduced words are cyclically reduced.
• FreeGroup.isConj_mk_iff_isRotated: cyclically reduced words represent conjugate elements exactly when they are rotations of each other.
• FreeGroup.isConj_iff_isRotated_reduceCyclically: the conjugacy criterion for elements of a free group.

The explicit cyclic-reduction conjugator uses Mathlib's FreeGroup.reduceCyclically.conj_conjugator_reduceCyclically from Mathlib.GroupTheory.FreeGroup.CyclicallyReduced.

References

• R. C. Lyndon and P. E. Schupp, Combinatorial Group Theory, Springer, 1977, Chapter I.

theorem FreeGroup.IsCyclicallyReduced.rotate {α : Type u_1} {L : List (α × Bool)} (h : IsCyclicallyReduced L) (n : ℕ) : IsCyclicallyReduced (L.rotate n)

A rotation of a cyclically reduced word is cyclically reduced.

theorem List.IsRotated.isCyclicallyReduced_iff {α : Type u_1} {L L' : List (α × Bool)} (h : L ~r L') : FreeGroup.IsCyclicallyReduced L ↔ FreeGroup.IsCyclicallyReduced L'

Cyclic reducedness is invariant under cyclic rotation.

@[simp]

theorem FreeGroup.isCyclicallyReduced_rotate {α : Type u_1} {L : List (α × Bool)} {n : ℕ} : IsCyclicallyReduced (L.rotate n) ↔ IsCyclicallyReduced L

A rotation of a word is cyclically reduced exactly when the word is.

theorem FreeGroup.conj_mk_rotate {α : Type u_1} (u : List (α × Bool)) (n : ℕ) : (mk (List.take (n % u.length) u))⁻¹ * mk u * mk (List.take (n % u.length) u) = mk (u.rotate n)

Rotating a word is conjugation by the inverse of its initial segment.

theorem FreeGroup.isConj_mk_of_isRotated {α : Type u_1} {u v : List (α × Bool)} (h : u ~r v) : IsConj (mk u) (mk v)

Two words related by a cyclic rotation represent conjugate elements of a free group. The words need not be reduced.

theorem FreeGroup.mk_conjugator_mul_mk_reduceCyclically {α : Type u_1} (L : List (α × Bool)) [DecidableEq α] : mk (reduceCyclically.conjugator L) * mk (reduceCyclically L) * (mk (reduceCyclically.conjugator L))⁻¹ = mk L

The cyclic reduction of any word has an explicit group conjugator.

theorem FreeGroup.isConj_mk_reduceCyclically {α : Type u_1} (L : List (α × Bool)) [DecidableEq α] : IsConj (mk L) (mk (reduceCyclically L))

The element of any word is conjugate to the element of its cyclic reduction.

theorem FreeGroup.isConj_of_isRotated_reduceCyclically {α : Type u_1} [DecidableEq α] {x y : FreeGroup α} (h : reduceCyclically x.toWord ~r reduceCyclically y.toWord) : IsConj x y

Elements whose cyclic reductions differ by a rotation are conjugate.

theorem FreeGroup.not_isCyclicallyReduced_append_append_invRev {α : Type u_1} {w : List (α × Bool)} (hw : w ≠ []) (L : List (α × Bool)) : ¬IsCyclicallyReduced (w ++ L ++ invRev w)

A word of the form w L w⁻¹ with w nonempty is not cyclically reduced: its first letter cancels against its last.

theorem FreeGroup.isConj_mk_iff_isRotated {α : Type u_1} {u v : List (α × Bool)} (hu : IsCyclicallyReduced u) (hv : IsCyclicallyReduced v) : IsConj (mk u) (mk v) ↔ u ~r v

Two cyclically reduced words represent conjugate elements of a free group exactly when they are cyclic rotations of each other.

theorem FreeGroup.isConj_iff_isRotated_reduceCyclically {α : Type u_1} [DecidableEq α] {x y : FreeGroup α} : IsConj x y ↔ reduceCyclically x.toWord ~r reduceCyclically y.toWord

Conjugacy criterion in free groups. Two elements of a free group are conjugate exactly when the cyclic reductions of their reduced words are cyclic rotations of each other.

theorem FreeGroup.not_isConj_of_mul_of_of_mul_inv_of {α : Type u_1} (a b c d : α) : ¬IsConj (of a * of b) (of c * (of d)⁻¹)

For any letters a, b, c and d, the elements a b and c d⁻¹ of a free group are not conjugate: the homomorphism to Multiplicative ℤ sending every generator to ofAdd 1 maps them to ofAdd 2 and ofAdd 0. In particular a b and a b⁻¹ are not conjugate.