English
Conjugation by an element of the centralizer preserves membership in the cycle factors finite set; the action by conjugation maps cycle factors to cycle factors within the same g.
Русский
Сопряжение элементом центральизатора сохраняет принадлежность к конечному множеству циклов факторов; действие сопряжения отображает циклические факторы в тот же набор.
LaTeX
$$ConjAct.toConjAct k • c ∈ g.cycleFactorsFinset$$
Lean4
theorem toConjAct_smul_mem_cycleFactorsFinset {k c : Perm α} (k_mem : k ∈ centralizer { g })
(c_mem : c ∈ g.cycleFactorsFinset) : ConjAct.toConjAct k • c ∈ g.cycleFactorsFinset :=
by
suffices (g.cycleFactorsFinset : Set (Perm α)) = (ConjAct.toConjAct k) • g.cycleFactorsFinset
by
rw [← Finset.mem_coe, this]
simp only [Set.smul_mem_smul_set_iff, Finset.mem_coe, c_mem]
have this := cycleFactorsFinset_conj_eq (ConjAct.toConjAct (k : Perm α)) g
rw [ConjAct.toConjAct_smul, mem_centralizer_singleton_iff.mp k_mem, mul_assoc] at this
simp only [mul_inv_cancel, mul_one] at this
conv_lhs => rw [this]
simp only [Finset.coe_smul_finset]
