commute_iff_of_mem_cycleFactorsFinset

English

For g,k,c with c ∈ g.cycleFactorsFinset, Commute k c is equivalent to the existence of a witness hc' such that k.subtypePerm hc' lies in zpowers of g.subtypePerm restricted to c’s support.

Русский

Для c ∈ cycleFactorsFinset g, Commute k c равносильно существованию hc', такого что k.subtypePerm hc' лежит в zpowers подгруппы g.subtypePerm, ограниченной на опоре c.

LaTeX

$$$\forall {g k c : \mathrm{Perm}(\alpha)} (hc : c ∈ g.\mathrm{cycleFactorsFinset}) :\\quad \mathrm{Commute}(k,c) \iff \\exists hc' : \forall x:\alpha, k x ∈ c.\mathrm{support} \iff x ∈ c.\mathrm{support},\; k.\mathrm{subtypePerm} hc' ∈ \mathrm{Subgroup.zpowers}(g.\mathrm{subtypePerm}(m\mathrm{emcycleFactorsFinset_support hc}))$$$

Lean4

theorem commute_iff_of_mem_cycleFactorsFinset [DecidableEq α] [Fintype α] {g k c : Equiv.Perm α}
    (hc : c ∈ g.cycleFactorsFinset) :
    Commute k c ↔
      ∃ hc' : ∀ x : α, k x ∈ c.support ↔ x ∈ c.support,
        k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm (mem_cycleFactorsFinset_support hc)) :=
  by
  rw [IsCycle.commute_iff' (mem_cycleFactorsFinset_iff.mp hc).1]
  apply exists_congr
  intro hc'
  simp only [Subgroup.mem_zpowers_iff]
  apply exists_congr
  intro n
  rw [Equiv.Perm.subtypePerm_on_cycleFactorsFinset hc]

Похожие утверждения