Powers of a cycle

A cycle f of a finite type has order the number n = f.support.card of points it moves (Equiv.Perm.IsCycle.orderOf), and every power f ^ k again moves either all of those points or none of them. This file computes the cycle type of such a power: whenever n ∤ k (equivalently, whenever f ^ k ≠ 1),

(f ^ k).cycleType = Multiset.replicate d (n / d) with n = f.support.card and d = n.gcd k,

so a nonidentity power f ^ k splits into gcd n k cycles of the common length n / gcd n k; for n ∣ k the power is the identity and its cycle type is empty. Mathlib computes the order of a power (orderOf_pow) and decides when a power of a cycle is again a cycle (Equiv.Perm.IsCycle.pow_iff) but does not compute the cycle type of one; the extra input is that all the cycles of f ^ k have the same length, which holds because (f ^ m) x = x is equivalent to orderOf f ∣ m independently of the point x of the support.

Main results

• Equiv.Perm.IsCycle.pow_apply_eq_self_iff: (f ^ n) x = x holds for one point moved by the cycle exactly when it holds for all of them, namely exactly when orderOf f ∣ n.
• Equiv.Perm.IsCycle.cycleType_pow_of_not_dvd: for n ∤ k, the cycle type of f ^ k is gcd n k copies of n / gcd n k.

The declarations are stated in the Equiv.Perm.IsCycle namespace, giving dot notation from hf : f.IsCycle, as upstream candidates.

References

• Mathlib PR #42723 (Kim Morrison) — the draft upstream adaptation of this file; the Equiv.Perm.IsCycle namespace, the orderOf-based statement of the fixed-point lemma, and the dropped support-card wrapper all follow the form prepared for that PR.

This supplies a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.1 and Lane G.7: the component permutation of the standard grid diagram of the (p, q) torus link is a power of the cyclic shift finRotate, and its cycle decomposition is what counts the components of the represented link.

@[simp]

theorem Equiv.Perm.IsCycle.pow_apply_eq_self_iff {β : Type u_1} [Finite β] {f : Perm β} (hf : f.IsCycle) {n : ℕ} {x : β} (hx : f x ≠ x) : (f ^ n) x = x ↔ orderOf f ∣ n

A power of a cycle fixes a point moved by the cycle exactly when the exponent is a multiple of the order of the cycle. Since the right-hand side does not depend on the point, a power of a cycle either moves every point the cycle moves, or fixes all of them.

theorem Equiv.Perm.IsCycle.cycleType_pow_of_not_dvd {α : Type u_1} [DecidableEq α] [Fintype α] {f : Perm α} (hf : f.IsCycle) {k : ℕ} (hk : ¬f.support.card ∣ k) : (f ^ k).cycleType = Multiset.replicate (f.support.card.gcd k) (f.support.card / f.support.card.gcd k)

The cycle type of a power of a cycle: writing n = f.support.card for the length of the cycle, the permutation f ^ k is a product of gcd n k disjoint cycles, each of length n / gcd n k.

The exponent is assumed not to be a multiple of n, which is exactly what rules out f ^ k = 1.