Recognizing cycles and transpositions in a permutation group

This file supplies recognition steps that read off structure of a permutation group from cycle data. A transitive subgroup of a finite symmetric group whose degree is prime contains a full cycle. A permutation with exactly one 2-cycle and all its other cycles of odd length has an odd power that is a transposition, and the exponent is given explicitly as the product of those odd lengths.

Both feed the recognition of a full symmetric group, which needs a primitive group containing a transposition: a transitive group of prime degree is primitive, and a transposition is what the second result produces. In the Galois-theoretic application the cycle pattern of the element fed to the second result is the degree pattern of a factorization of a polynomial modulo a prime, read through the Frobenius element.

A subgroup of Sₙ, n ≥ 5, of index less than n contains Aₙ. This recognizes the large subgroups in the low-degree classification, where the order of a subgroup bounds its index.

Main results

• TauCeti.card_dvd_natCard_and_natCard_dvd_factorial_of_isPretransitive: the order of a transitive permutation group of degree n is a multiple of n and a divisor of n !.
• TauCeti.exists_isCycle_mem_of_isPretransitive_of_prime_card: a transitive permutation group of prime degree contains a full cycle.
• TauCeti.subgroup_eq_top_of_isPretransitive_of_prime_card_of_isSwap_mem: a transitive permutation group of prime degree that contains a transposition is the full symmetric group.
• TauCeti.alternatingGroup_le_of_isPretransitive_of_orderOf_eq_three: a transitive subgroup of S₅ containing an element of order 3 contains A₅.
• TauCeti.subgroup_eq_top_of_isPretransitive_of_orderOf_eq_six: a transitive subgroup of S₅ containing an element of order 6 is the full symmetric group.
• TauCeti.alternatingGroup_le_of_index_lt: a subgroup of Sₙ, n ≥ 5, of index less than n contains Aₙ.
• Equiv.Perm.cycleType_eq_two_three_of_orderOf_eq_six: an order-six permutation on five points has cycle type (2, 3).
• Equiv.Perm.isThreeCycle_of_orderOf_eq_three: an order-three permutation on five points is a three-cycle.
• Equiv.Perm.isSwap_pow_prod_erase_two_cycleType_and_odd: if a permutation has exactly one 2-cycle and all its other cycles have odd length, an explicit odd power is a transposition.
• Equiv.Perm.exists_odd_isSwap_pow: the corresponding existential form.

theorem TauCeti.card_dvd_natCard_and_natCard_dvd_factorial_of_isPretransitive {α : Type u_1} [Fintype α] (G : Subgroup (Equiv.Perm α)) [MulAction.IsPretransitive (↥G) α] [Nonempty α] : Fintype.card α ∣ Nat.card ↥G ∧ Nat.card ↥G ∣ (Fintype.card α).factorial

The order of a transitive permutation group on a nonempty finite set α is a multiple of the degree Fintype.card α, by TauCeti.natCard_dvd_natCard_of_isPretransitive, and a divisor of (Fintype.card α)!, by Lagrange's theorem.

theorem TauCeti.exists_isCycle_mem_of_isPretransitive_of_prime_card {α : Type u_1} [Fintype α] [DecidableEq α] {G : Subgroup (Equiv.Perm α)} (hG : MulAction.IsPretransitive (↥G) α) (hp : Nat.Prime (Fintype.card α)) : ∃ g ∈ G, g.IsCycle ∧ g.support = Finset.univ

A transitive permutation group of prime degree contains a full cycle.

The returned permutation has order and support cardinality equal to the degree, so its support is all of α. This is intended as a prime-degree recognition input for the low-degree classification and for the prime-degree branch of the Sₙ realization argument.

theorem TauCeti.subgroup_eq_top_of_isPretransitive_of_prime_card_of_isSwap_mem {β : Type u_2} [DecidableEq β] {G : Subgroup (Equiv.Perm β)} (hG : MulAction.IsPretransitive (↥G) β) (hp : Nat.Prime (Nat.card β)) (g : Equiv.Perm β) (hgSwap : g.IsSwap) (hg : g ∈ G) : G = ⊤

A transitive subgroup of a symmetric group of prime degree that contains a transposition is the full symmetric group, the prime-degree form of Jordan's transposition recognition theorem.

This recognition result identifies Galois groups from an irreducible polynomial and a factorization pattern exhibiting a transposition.

theorem TauCeti.alternatingGroup_le_of_index_lt {α : Type u_1} [Fintype α] [DecidableEq α] (hα : 5 ≤ Nat.card α) {H : Subgroup (Equiv.Perm α)} (hH : H.index < Nat.card α) : alternatingGroup α ≤ H

A subgroup of the symmetric group on n ≥ 5 points whose index is less than n contains the alternating group.

theorem Equiv.Perm.isSwap_pow_prod_erase_two_cycleType_and_odd {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} (htwo : Multiset.count 2 σ.cycleType = 1) (hodd : ∀ n ∈ σ.cycleType, n ≠ 2 → Odd n) : (σ ^ (σ.cycleType.erase 2).prod).IsSwap ∧ Odd (σ.cycleType.erase 2).prod

If a permutation has exactly one cycle of length two and every other cycle has odd length, then raising it to the product of those other cycle lengths gives a transposition.

The exponent is itself odd. This is the cycle-theoretic step used to turn a factorization pattern with one quadratic factor and only odd-degree remaining factors into a transposition in a Galois group.

theorem Equiv.Perm.exists_odd_isSwap_pow {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} (htwo : Multiset.count 2 σ.cycleType = 1) (hodd : ∀ n ∈ σ.cycleType, n ≠ 2 → Odd n) : ∃ (k : ℕ), Odd k ∧ (σ ^ k).IsSwap

A permutation with exactly one 2-cycle and all remaining cycle lengths odd has an odd power that is a transposition.

theorem Equiv.Perm.cycleType_eq_two_three_of_orderOf_eq_six {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} (hcard : Fintype.card α = 5) (hσ : orderOf σ = 6) : σ.cycleType = {2, 3}

A permutation of order 6 on five points has cycle type (2, 3): it is the product of a transposition and a three-cycle.

theorem Equiv.Perm.isThreeCycle_of_orderOf_eq_three {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Perm α} (hcard : Fintype.card α = 5) (hσ : orderOf σ = 3) : σ.IsThreeCycle

A permutation of order 3 on five points is a three-cycle.

theorem TauCeti.alternatingGroup_le_of_isPretransitive_of_orderOf_eq_three {α : Type u_1} [Fintype α] [DecidableEq α] (hcard : Fintype.card α = 5) {G : Subgroup (Equiv.Perm α)} (hG : MulAction.IsPretransitive (↥G) α) {σ : Equiv.Perm α} (hσ : orderOf σ = 3) (hg : σ ∈ G) : alternatingGroup α ≤ G

A transitive subgroup of S₅ containing an element of order 3 contains the alternating group. On five points an element of order 3 is a three-cycle, so a primitive criterion applies: a primitive subgroup of Sₙ, n ≥ 3, containing a three-cycle contains Aₙ.

theorem TauCeti.subgroup_eq_top_of_isPretransitive_of_orderOf_eq_six {β : Type u_2} (hcard : Nat.card β = 5) {G : Subgroup (Equiv.Perm β)} (hG : MulAction.IsPretransitive (↥G) β) {σ : Equiv.Perm β} (hσ : orderOf σ = 6) (hg : σ ∈ G) : G = ⊤

A transitive subgroup of S₅ containing an element of order 6 is the full symmetric group. On five points an element of order 6 is the product of a transposition and a three-cycle, so some odd power of it is a transposition and the transposition criterion applies.