English
Conjugating both g and a cycle c by an arbitrary permutation k preserves the cycle-factor property: k c k^{-1} is a cycle factor of k g k^{-1} iff c is a cycle factor of g.
Русский
Сопряжение перестановок c и g конъюгированием k сохраняет свойство быть циклом: k c k^{-1} — цикл-фактор для k g k^{-1} тогда и только тогда, когда c — цикл-фактор для g.
LaTeX
$$$\forall g,k,c : \mathrm{Perm}(\alpha),\; k c k^{-1} \in (k g k^{-1}).\mathrm{cycleFactorsFinset} \iff c \in g.\mathrm{cycleFactorsFinset}$$$
Lean4
/-- A permutation `c` is a cycle of `g` iff `k * c * k⁻¹` is a cycle of `k * g * k⁻¹` -/
theorem mem_cycleFactorsFinset_conj (g k c : Perm α) :
k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset :=
by
suffices imp_lemma : ∀ {g k c : Perm α}, c ∈ g.cycleFactorsFinset → k * c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
by
refine ⟨fun h ↦ ?_, imp_lemma⟩
have aux : ∀ h : Perm α, h = k⁻¹ * (k * h * k⁻¹) * k := fun _ ↦ by group
rw [aux g, aux c]
exact imp_lemma h
intro g k c
simp only [mem_cycleFactorsFinset_iff]
apply And.imp IsCycle.conj
intro hc a ha
simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]
apply hc
rw [mem_support] at ha ⊢
contrapose! ha
simp only [mul_smul, ← Perm.smul_def] at ha ⊢
rw [ha]
simp only [Perm.smul_def, apply_inv_self]
