Cycles of permutations intertwined by a map

Let f : α → β intertwine a permutation σ of α with a permutation τ of β, that is f (σ x) = τ (f x) for every x (Function.Semiconj f σ τ). Then f carries the cycle of x onto the cycle of f x, going round it a whole number of times. This file records the resulting relations between the cycle data of σ and of τ:

• Function.Semiconj.minimalPeriod_dvd: the length of the cycle of f x divides the length of the cycle of x.
• Function.Semiconj.ncard_sameCycle_and_eq_mul_minimalPeriod: more precisely, the length of the cycle of x is the length of the cycle of f x times the number of points of the cycle of x that lie in the fibre of f through x.
• TauCeti.orbitCount_le_mul_orbitCount_of_semiconj: if every fibre of f has at most s points, then σ has at most s times as many cycles as τ.

The typical instance is a permutation preserving a partition of α into blocks, with f the map sending a point to its block and τ the induced permutation of the blocks. The cycle of a block then has length the cycle length of any of its points divided by the number of points that cycle has in the block.

theorem Function.Semiconj.minimalPeriod_dvd {α : Type u_1} {β : Type u_2} {f : α → β} {fa : α → α} {fb : β → β} (h : Semiconj f fa fb) (x : α) : minimalPeriod fb (f x) ∣ minimalPeriod fa x

If f intertwines fa with fb, the minimal period of f x under fb divides the minimal period of x under fa. When x is not periodic the right side is 0.

theorem Function.Semiconj.setOf_sameCycle_and_eq {α : Type u_1} {β : Type u_2} {f : α → β} {σ : Equiv.Perm α} {τ : Equiv.Perm β} (h : Semiconj f ⇑σ ⇑τ) (x : α) : {y : α | σ.SameCycle x y ∧ f y = f x} = {y : α | (σ ^ minimalPeriod (⇑τ) (f x)).SameCycle x y}

If f intertwines the permutations σ and τ, the points of the cycle of x that f sends to f x form a single cycle of σ ^ k, where k is the length of the cycle of f x.

theorem Function.Semiconj.ncard_sameCycle_and_eq_mul_minimalPeriod {α : Type u_1} {β : Type u_2} {f : α → β} {σ : Equiv.Perm α} {τ : Equiv.Perm β} [Finite α] (h : Semiconj f ⇑σ ⇑τ) (x : α) : {y : α | σ.SameCycle x y ∧ f y = f x}.ncard * minimalPeriod (⇑τ) (f x) = minimalPeriod (⇑σ) x

The cycle of a point wraps round the cycle of its image. If f intertwines the permutations σ and τ of finite types, the length of the cycle of x is the length of the cycle of f x times the number of points of the cycle of x lying in the fibre of f through x.

theorem TauCeti.orbitCount_le_mul_orbitCount_of_semiconj {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] {f : α → β} {σ : Equiv.Perm α} {τ : Equiv.Perm β} (h : Function.Semiconj f ⇑σ ⇑τ) {s : ℕ} (hs : ∀ (y : β), (f ⁻¹' {y}).ncard ≤ s) : orbitCount σ ≤ s * orbitCount τ

If f intertwines the permutations σ and τ of finite types and every fibre of f has at most s points, then σ has at most s times as many cycles as τ.