English
A permutation g commutes with a cycle c if and only if g preserves the support of c and acts on it as a power of c.
Русский
Перестановка g коммутирует с циклом c тогда и только тогда, когда g сохраняет опору c и действует на ней как степень c.
LaTeX
$$$\\text{Commute}(g,c) \\iff \\exists hc' : ∀x, g x \\in \\operatorname{supp}(c) \\leftrightarrow x \\in \\operatorname{supp}(c) \\land g|_{\\operatorname{supp}(c)} = c^{n}$$$
Lean4
/-- A permutation `g` commutes with a cycle `c` if and only if
`c.support` is invariant under `g`, and `g` acts on it as a power of `c`. -/
theorem commute_iff {g c : Perm α} (hc : c.IsCycle) :
Commute g c ↔
∃ hc' : ∀ x : α, g x ∈ c.support ↔ x ∈ c.support, ofSubtype (subtypePerm g hc') ∈ Subgroup.zpowers c :=
by
simp_rw [hc.commute_iff', Subgroup.mem_zpowers_iff]
refine exists_congr fun hc' => exists_congr fun k => ?_
rw [subtypePermOfSupport, subtypePerm_zpow c k]
simp only [Perm.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
apply forall_congr'
intro a
by_cases ha : a ∈ c.support
· rw [imp_iff_right ha, ofSubtype_subtypePerm_of_mem hc' ha]
· rw [iff_true_left (fun b ↦ (ha b).elim), ofSubtype_apply_of_not_mem, ← notMem_support]
· exact Finset.notMem_mono (support_zpow_le c k) ha
· exact ha
