Some lemmas pertaining to the action of ConjAct (Perm α) on Perm α

We prove some lemmas related to the conjugation action of Perm α on Perm α:

Let α be a decidable fintype.

• support_conj_eq_smul_support relates the support of MulAut.conj k g with that of g.

• cycleFactorsFinset_conj_eq, mem_cycleFactorsFinset_conj' and cycleFactorsFinset_conj relate the set of cycles of g, g.cycleFactorsFinset, with that for MulAut.conj k g.

theorem Equiv.Perm.mem_conj_support {α : Type u_1} [DecidableEq α] [Fintype α] (k g : Perm α) (a : α) : a ∈ ((MulAut.conj k) g).support ↔ k⁻¹ a ∈ g.support

a : α belongs to the support of MulAut.conj k g iff k⁻¹ a belongs to the support of g

theorem Equiv.Perm.support_conj_eq_smul_support {α : Type u_1} [DecidableEq α] [Fintype α] (k g : Perm α) : ((MulAut.conj k) g).support = k • g.support

@[deprecated Equiv.Perm.support_conj_eq_smul_support (since := "2026-09-21")]

theorem Equiv.Perm.support_toConjAct_eq_smul_support {α : Type u_1} [DecidableEq α] [Fintype α] (k g : Perm α) : ((MulAut.conj k) g).support = k • g.support

Alias of Equiv.Perm.support_conj_eq_smul_support.

theorem Equiv.Perm.cycleFactorsFinset_conj {α : Type u_1} [DecidableEq α] [Fintype α] (g k : Perm α) : ((MulAut.conj k) g).cycleFactorsFinset = Finset.map (MulAut.conj k).toEmbedding g.cycleFactorsFinset

theorem Equiv.Perm.mem_cycleFactorsFinset_conj' {α : Type u_1} [DecidableEq α] [Fintype α] (k g c : Perm α) : (MulAut.conj k) c ∈ ((MulAut.conj k) g).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

A permutation c is a cycle of g iff k • c is a cycle of k • g

theorem Equiv.Perm.cycleFactorsFinset_conj_eq {α : Type u_1} [DecidableEq α] [Fintype α] (k g : Perm α) : ((MulAut.conj k) g).cycleFactorsFinset = MulAut.conj k • g.cycleFactorsFinset

theorem Equiv.Perm.conj_smul_range_ofSubtype {α : Type u_1} [DecidableEq α] [Finite α] (g : Perm α) (s : Finset α) : MulAut.conj g • ofSubtype.range = ofSubtype.range