Subgroups generated by transpositions

This file studies subgroups generated by transpositions.

Main results

• swap_mem_closure_isSwap : If a subgroup is generated by transpositions, then a transposition swap x y lies in the subgroup if and only if x lies in the same orbit as y.
• mem_closure_isSwap : If a subgroup is generated by transpositions, then a permutation f lies in the subgroup if and only if f has finite support and f x always lies in the same orbit as x.

theorem finite_compl_fixedBy_closure_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {S : Set G} : (∀ g ∈ Subgroup.closure S, (MulAction.fixedBy α g)ᶜ.Finite) ↔ ∀ g ∈ S, (MulAction.fixedBy α g)ᶜ.Finite

If the support of each element in a generating set of a permutation group is finite, then the support of every element in the group is finite.

theorem exists_smul_not_mem_of_subset_orbit_closure {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (S : Set G) (T : Set α) {a : α} (hS : ∀ g ∈ S, g⁻¹ ∈ S) (subset : T ⊆ MulAction.orbit (↥(Subgroup.closure S)) a) (not_mem : a ∉ T) (nonempty : T.Nonempty) : ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T

Given a symmetric generating set of a permutation group, if T is a nonempty proper subset of an orbit, then there exists a generator that sends some element of T into the complement of T.

theorem finite_compl_fixedBy_swap {α : Type u_2} [DecidableEq α] {x : α} {y : α} : (MulAction.fixedBy α (Equiv.swap x y))ᶜ.Finite

theorem Equiv.Perm.IsSwap.finite_compl_fixedBy {α : Type u_2} [DecidableEq α] {σ : Equiv.Perm α} (h : σ.IsSwap) : (MulAction.fixedBy α σ)ᶜ.Finite

theorem SubmonoidClass.swap_mem_trans {α : Type u_2} [DecidableEq α] {a : α} {b : α} {c : α} {C : Type u_3} [SetLike C (Equiv.Perm α)] [SubmonoidClass C (Equiv.Perm α)] (M : C) (hab : Equiv.swap a b ∈ M) (hbc : Equiv.swap b c ∈ M) : Equiv.swap a c ∈ M

theorem swap_mem_closure_isSwap {α : Type u_2} [DecidableEq α] {S : Set (Equiv.Perm α)} (hS : ∀ f ∈ S, f.IsSwap) {x : α} {y : α} : Equiv.swap x y ∈ Subgroup.closure S ↔ x ∈ MulAction.orbit (↥(Subgroup.closure S)) y

If a subgroup is generated by transpositions, then a transposition swap x y lies in the subgroup if and only if x lies in the same orbit as y.

theorem mem_closure_isSwap {α : Type u_2} [DecidableEq α] {S : Set (Equiv.Perm α)} (hS : ∀ f ∈ S, f.IsSwap) {f : Equiv.Perm α} : f ∈ Subgroup.closure S ↔ (MulAction.fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), f x ∈ MulAction.orbit (↥(Subgroup.closure S)) x

If a subgroup is generated by transpositions, then a permutation f lies in the subgroup if and only if f has finite support and f x always lies in the same orbit as x.

theorem mem_closure_isSwap' {α : Type u_2} [DecidableEq α] {f : Equiv.Perm α} : f ∈ Subgroup.closure {σ : Equiv.Perm α | σ.IsSwap} ↔ (MulAction.fixedBy α f)ᶜ.Finite

A permutation is a product of transpositions if and only if it has finite support.

theorem closure_of_isSwap_of_isPretransitive {α : Type u_2} [DecidableEq α] [Finite α] {S : Set (Equiv.Perm α)} (hS : ∀ σ ∈ S, σ.IsSwap) [MulAction.IsPretransitive (↥(Subgroup.closure S)) α] : Subgroup.closure S = ⊤

A transitive permutation group generated by transpositions must be the whole symmetric group

theorem surjective_of_isSwap_of_isPretransitive {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Finite α] (S : Set G) (hS1 : ∀ σ ∈ S, ((MulAction.toPermHom G α) σ).IsSwap) (hS2 : Subgroup.closure S = ⊤) [h : MulAction.IsPretransitive G α] : Function.Surjective ⇑(MulAction.toPermHom G α)

A transitive permutation group generated by transpositions must be the whole symmetric group