Closure results for permutation groups #
- This file contains several closure results:
closure_isCycle: The symmetric group is generated by cyclesclosure_cycle_adjacent_swap: The symmetric group is generated by a cycle and an adjacent transpositionclosure_cycle_coprime_swap: The symmetric group is generated by a cycle and a coprime transpositionclosure_prime_cycle_swap: The symmetric group is generated by a prime cycle and a transposition
theorem
Equiv.Perm.closure_isCycle
{β : Type u_3}
[Finite β]
:
Subgroup.closure {σ : Equiv.Perm β | σ.IsCycle} = ⊤
theorem
Equiv.Perm.closure_cycle_adjacent_swap
{α : Type u_2}
[DecidableEq α]
[Fintype α]
{σ : Equiv.Perm α}
(h1 : σ.IsCycle)
(h2 : σ.support = Finset.univ)
(x : α)
:
Subgroup.closure {σ, Equiv.swap x (σ x)} = ⊤
theorem
Equiv.Perm.closure_cycle_coprime_swap
{α : Type u_2}
[DecidableEq α]
[Fintype α]
{n : ℕ}
{σ : Equiv.Perm α}
(h0 : n.Coprime (Fintype.card α))
(h1 : σ.IsCycle)
(h2 : σ.support = Finset.univ)
(x : α)
:
Subgroup.closure {σ, Equiv.swap x ((σ ^ n) x)} = ⊤
theorem
Equiv.Perm.closure_prime_cycle_swap
{α : Type u_2}
[DecidableEq α]
[Fintype α]
{σ τ : Equiv.Perm α}
(h0 : Nat.Prime (Fintype.card α))
(h1 : σ.IsCycle)
(h2 : σ.support = Finset.univ)
(h3 : τ.IsSwap)
:
Subgroup.closure {σ, τ} = ⊤