English
For g,k,c with c ∈ g.cycleFactorsFinset, Commute k c holds iff there exists a function hc' describing how k acts on c's support such that k.subtypePerm hc' lies in the zpowers subgroup determined by g.subtypePerm restricted to the support of c.
Русский
Пусть c ∈ cycleFactorsFinset g. Тогда Commute k c эквивалентно существованию hc', описывающего действие k на опору c так, что k.subtypePerm hc' лежит в zpowers подгруппе, порожденной g.subtypePerm на опоре c.
LaTeX
$$$\forall {α} [DecidableEq α] [Fintype α] {g k c : \mathrm{Perm}(α)}\; (hc : c ∈ g.\mathrm{cycleFactorsFinset}) :\\quad \mathrm{Commute}(k,c) \iff \\exists hc' : \forall x:α, k x ∈ c.\mathrm{support} \iff x ∈ c.\mathrm{support},\; k.\mathrm{subtypePerm} hc' ∈ \mathrm{Subgroup.zpowers}(g.\mathrm{subtypePerm}(m\emph{emcycleFactorsFinset_support hc}))$$$
Lean4
theorem forall_commute_iff [DecidableEq α] [Fintype α] (g z : Perm α) :
(∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔
∀ c ∈ g.cycleFactorsFinset,
∃ (hc : ∀ x : α, z x ∈ c.support ↔ x ∈ c.support), ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c :=
by
apply forall_congr'
intro c
apply imp_congr_right
intro hc
exact IsCycle.commute_iff (mem_cycleFactorsFinset_iff.mp hc).1
