Documentation

TauCeti.GroupTheory.Perm.TransitiveGroupLabel.Solvable

Solvable transitive subgroups of the symmetric groups of degree at most five #

This file determines the solvability column of the table of transitive groups of degree at most five. In degree at most four every reference subgroup is solvable, because the whole symmetric group on at most four points is (Mathlib's Equiv.Perm.isSolvable). In degree five the labels 5T1, 5T2 and 5T3 are solvable, while 5T4 = A₅ and 5T5 = S₅ are not.

The solvable transitive subgroups of Equiv.Perm (Fin 5) are precisely the subgroups conjugate into the Frobenius group 5T3 of order twenty. The forward implication uses the classification of transitive subgroups: 5T1, 5T2, and 5T3 lie in 5T3, while 5T4 = A₅ and 5T5 = S₅ are not solvable. The reverse implication follows because 5T3 is solvable.

The solvability of 5T3 comes from its normal cyclic subgroup 5T1 of order five. The quotient has order four, hence is commutative, so both the subgroup and quotient are solvable.

Solvability of a permutation group with a transitive-group label depends only on the label (TauCeti.TransitiveGroupLabel.isSolvable_iff), so the table applies to every transitive subgroup of degree at most five.

Main results #

source
theorem TauCeti.isSolvable_referenceSubgroup_five_two :
Group.IsSolvable ↥(referenceSubgroup 5 ⟨2, isSolvable_referenceSubgroup_five_two._proof_1⟩)

The reference subgroup 5T3, the Frobenius group of order twenty, is solvable.

source
theorem TauCeti.isSolvable_referenceSubgroup_five_zero :
Group.IsSolvable ↥(referenceSubgroup 5 ⟨0, isSolvable_referenceSubgroup_five_zero._proof_1⟩)

The cyclic reference subgroup 5T1 is solvable.

source
theorem TauCeti.isSolvable_referenceSubgroup_five_one :
Group.IsSolvable ↥(referenceSubgroup 5 ⟨1, isSolvable_referenceSubgroup_five_one._proof_1⟩)

The dihedral reference subgroup 5T2 is solvable.

source
theorem TauCeti.not_isSolvable_referenceSubgroup_five_three :
¬Group.IsSolvable ↥(referenceSubgroup 5 ⟨3, not_isSolvable_referenceSubgroup_five_three._proof_1⟩)

The alternating reference subgroup 5T4 is not solvable.

source
theorem TauCeti.not_isSolvable_referenceSubgroup_five_four :
¬Group.IsSolvable ↥(referenceSubgroup 5 ⟨4, not_isSolvable_referenceSubgroup_five_four._proof_1⟩)

The full symmetric reference subgroup 5T5 is not solvable.

source
theorem TauCeti.isSolvable_referenceSubgroup_five_iff (j : TransitiveGroupIndex 5) :
Group.IsSolvable ↥(referenceSubgroup 5 j) ↔ ↑j < 3

A degree-five reference subgroup is solvable exactly for the labels 5T1, 5T2, and 5T3.

source
@[simp]
theorem TauCeti.isSolvable_referenceSubgroup_iff {n : ℕ} (j : TransitiveGroupIndex n) :
Group.IsSolvable ↥(referenceSubgroup n j) ↔ n ≠ 5 ∨ ↑j < 3

The solvability column of the table of transitive groups of degree at most five. A reference subgroup is solvable unless its label is 5T4 or 5T5, the alternating and symmetric groups on five points.

source
theorem TauCeti.TransitiveGroupLabel.isSolvable_iff_ne_five_or_lt_three {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) :
Group.IsSolvable ↥G ↔ n ≠ 5 ∨ ↑j < 3

A permutation group with a transitive-group label is solvable unless its label is 5T4 or 5T5.

source
theorem TauCeti.isSolvable_iff_exists_le_map_conj_referenceSubgroup_five_two (G : Subgroup (Equiv.Perm (Fin 5))) [MulAction.IsPretransitive (↥G) (Fin 5)] :
Group.IsSolvable ↥G ↔ ∃ (τ : Equiv.Perm (Fin 5)), G ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) (referenceSubgroup 5 ⟨2, isSolvable_referenceSubgroup_five_two._proof_1⟩)

Solvable transitive subgroups of S₅. A transitive subgroup of the symmetric group on five points is solvable if and only if it is contained in a conjugate of the Frobenius reference subgroup 5T3.