English
The centralizer of a cycle is generated by powers of that cycle on its support.
Русский
Централизатор цикла порождается степенями этого цикла на его опоре.
LaTeX
$$$\\operatorname{Commute}(g,c) \\iff \\exists hc' \\in \\mathrm{zpowers}(c.subtypePermOfSupport) \\text{ such that } g.subtypePerm hc' = c.subtypePermOfSupport$$$
Lean4
/-- Centralizer of a cycle is a power of that cycle on the cycle -/
theorem commute_iff' {g c : Perm α} (hc : c.IsCycle) :
Commute g c ↔
∃ hc' : ∀ x : α, g x ∈ c.support ↔ x ∈ c.support, subtypePerm g hc' ∈ Subgroup.zpowers c.subtypePermOfSupport :=
by
constructor
· intro hgc
have hgc' := mem_support_iff_of_commute hgc
use hgc'
obtain ⟨a, ha⟩ := IsCycle.nonempty_support hc
obtain ⟨i, hi⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp ((hgc' a).mpr ha))
use i
ext ⟨x, hx⟩
simp only [subtypePermOfSupport, Subtype.coe_mk, subtypePerm_apply]
rw [subtypePerm_apply_zpow_of_mem]
obtain ⟨j, rfl⟩ := hc.sameCycle (mem_support.mp ha) (mem_support.mp hx)
simp only [← mul_apply, Commute.eq (Commute.zpow_right hgc j)]
rw [← zpow_add, add_comm i j, zpow_add]
simp only [mul_apply, EmbeddingLike.apply_eq_iff_eq]
exact hi
· rintro ⟨hc', ⟨i, hi⟩⟩
ext x
simp only [coe_mul, Function.comp_apply]
by_cases hx : x ∈ c.support
· suffices hi' : ∀ x ∈ c.support, g x = (c ^ i) x
by
rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]
simp only [← mul_apply, ← zpow_add_one, ← zpow_one_add, add_comm]
intro x hx
have hix := Perm.congr_fun hi ⟨x, hx⟩
simp only [← Subtype.coe_inj, subtypePermOfSupport, subtypePerm_apply, subtypePerm_apply_zpow_of_mem] at hix
exact hix.symm
· rw [notMem_support.mp hx, eq_comm, ← notMem_support]
contrapose! hx
exact (hc' x).mp hx
