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

We prove some lemmas related to the action of ConjAct (Perm α) on Perm α:

Let α be a decidable fintype.

• conj_support_eq relates the support of 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 k • g

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

a : α belongs to the support of k • g iff k⁻¹ * a belongs to the support of g

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

@[simp]

theorem Equiv.Perm.mem_cycleFactorsFinset_conj' {α : Type u_1} [DecidableEq α] [Fintype α] (k : ConjAct (Perm α)) (g c : Perm α) : k • c ∈ (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 : ConjAct (Perm α)) (g : Perm α) : (k • g).cycleFactorsFinset = k • g.cycleFactorsFinset