Transitive subgroups of S₃, S₄ and S₅

This file classifies the transitive subgroups of the symmetric groups on three, four and five points up to conjugacy: each of them is conjugate to exactly one of the reference subgroups of TauCeti.referenceSubgroup, so it carries exactly one of the labels 3T1, 3T2, respectively 4T1, …, 4T5, respectively 5T1, …, 5T5.

The existence half runs through the order of the subgroup. A transitive subgroup of Equiv.Perm (Fin n) has order divisible by n, by the orbit-stabilizer theorem, and dividing n !.

• In degree three the order is 3 or 6. Order 6 is the whole group, and order 3 is index two, so it is the alternating group, which is the reference subgroup of 3T1.
• In degree four the order is 4, 8, 12 or 24. Order 24 is the whole group and order 12 is the alternating group, as in degree three. Order 8 is a Sylow 2-subgroup, and so is the reference subgroup of 4T3, so the two are conjugate by Sylow's theorem. Order 4 acts regularly: if the subgroup contains an element of order four, that element is a four-cycle, it generates the subgroup, and conjugating it onto finRotate 4 gives 4T1; otherwise every nontrivial element is a fixed-point-free involution, that is a double transposition, and the subgroup is the Klein four-group of 4T2.
• In degree five the order is 5, 10, 20, 60 or 120 (TauCeti.natCard_mem_of_natCard_eq_five_of_isPretransitive). Orders 120 and 60 are the whole group and the alternating group. A subgroup of order dividing 20 has a unique Sylow 5-subgroup, so it lies in the normalizer of that subgroup; conjugating the Sylow subgroup onto the rotation group 5T1 carries the subgroup between 5T1 and its normalizer, the Frobenius group 5T3 of affine maps of ℤ/5. A subgroup of order 10 in between has index two in 5T3, so it contains the square of every element of 5T3, and in particular the square i ↦ 3 - i of i ↦ 2 i + 1, which generates 5T2 together with the rotation.

The uniqueness half compares invariants: the orders of the reference subgroups in each degree are pairwise distinct, except for 4T1 and 4T2, which have order four and are told apart by parity, since 4T1 contains the odd permutation finRotate 4.

On the way, the orders of the reference subgroups of degrees three, four and five are computed, the reference subgroup of 3T1 is identified with the alternating group, that of 4T3 with the centralizer of the double transposition finRotate 4 ^ 2, and that of 5T3 with the normalizer of the rotation group 5T1.

Main results

• TauCeti.natCard_referenceSubgroup_three_zero, …, TauCeti.natCard_referenceSubgroup_five_four: the orders 3, 6, 4, 4, 8, 12, 24 and 5, 10, 20, 60, 120 of the reference subgroups in degrees three, four and five.
• TauCeti.not_isCyclic_referenceSubgroup_four_one: the reference subgroup of 4T2 is not cyclic, unlike that of 4T1 (TauCeti.isCyclic_referenceSubgroup_index_zero).
• TauCeti.index_referenceSubgroup_five_two: the reference subgroup of 5T3 has index six.
• TauCeti.not_isSwap_of_mem_referenceSubgroup_five_two: the reference subgroup of 5T3 contains no transposition.
• TauCeti.referenceSubgroup_five_two_eq_normalizer_referenceSubgroup_five_zero: the reference subgroup of 5T3 is the normalizer of that of 5T1.
• TauCeti.referenceSubgroup_three_zero_le_alternatingGroup, TauCeti.not_referenceSubgroup_three_one_le_alternatingGroup: the parities of 3T1 and 3T2, TauCeti.referenceSubgroup_four_le_alternatingGroup_iff: the parities of the five quartic labels, and TauCeti.referenceSubgroup_five_le_alternatingGroup_iff: the parities of the five quintic labels.
• TauCeti.exists_le_map_conj_referenceSubgroup_four_two_iff: a reference subgroup of degree four lies in a conjugate of the dihedral group of 4T3 exactly for the labels 4T1, 4T2 and 4T3.
• TauCeti.TransitiveGroupLabel.eq_of_three, TauCeti.TransitiveGroupLabel.eq_of_four, TauCeti.TransitiveGroupLabel.eq_of_five: in degrees three, four and five a subgroup carries at most one label.
• TauCeti.existsUnique_transitiveGroupLabel_three, TauCeti.existsUnique_transitiveGroupLabel_four, TauCeti.existsUnique_transitiveGroupLabel_five: a transitive subgroup of the symmetric group on three, four, respectively five, points carries exactly one label.
• TauCeti.exists_transitiveGroupLabel_three_iff, TauCeti.exists_transitiveGroupLabel_four_iff, TauCeti.exists_transitiveGroupLabel_five_iff: a subgroup carries a label exactly when it is transitive.

References

• J. D. Dixon and B. Mortimer, Permutation Groups, GTM 163, Springer, 1996, §2 and Appendix B.
• LMFDB, Transitive groups, entries of degrees three, four and five.

Preliminaries

Degree three

theorem TauCeti.closure_finRotate_three_eq_alternatingGroup : Subgroup.closure {finRotate 3} = alternatingGroup (Fin 3)

The reference subgroup of 3T1, generated by the rotation of three points, is the alternating group.

theorem TauCeti.natCard_referenceSubgroup_three_zero : Nat.card ↥(referenceSubgroup 3 ⟨0, natCard_referenceSubgroup_three_zero._proof_1⟩) = 3

The reference subgroup of 3T1 has order 3.

theorem TauCeti.natCard_referenceSubgroup_three_one : Nat.card ↥(referenceSubgroup 3 ⟨1, natCard_referenceSubgroup_three_one._proof_1⟩) = 6

The reference subgroup of 3T2 has order 6.

theorem TauCeti.referenceSubgroup_three_zero_le_alternatingGroup : referenceSubgroup 3 ⟨0, natCard_referenceSubgroup_three_zero._proof_1⟩ ≤ alternatingGroup (Fin 3)

The reference subgroup of 3T1 consists of even permutations.

theorem TauCeti.not_referenceSubgroup_three_one_le_alternatingGroup : ¬referenceSubgroup 3 ⟨1, natCard_referenceSubgroup_three_one._proof_1⟩ ≤ alternatingGroup (Fin 3)

The reference subgroup of 3T2 is not contained in the alternating group: it contains the odd permutation swap 0 1.

theorem TauCeti.exists_transitiveGroupLabel_three (G : Subgroup (Equiv.Perm (Fin 3))) [MulAction.IsPretransitive (↥G) (Fin 3)] : ∃ (j : TransitiveGroupIndex 3), TransitiveGroupLabel j G

Every transitive subgroup of the symmetric group on three points carries a label.

theorem TauCeti.TransitiveGroupLabel.eq_of_three {j k : TransitiveGroupIndex 3} {G : Subgroup (Equiv.Perm (Fin 3))} (hj : TransitiveGroupLabel j G) (hk : TransitiveGroupLabel k G) : j = k

A subgroup of the symmetric group on three points carries at most one label.

theorem TauCeti.existsUnique_transitiveGroupLabel_three (G : Subgroup (Equiv.Perm (Fin 3))) [MulAction.IsPretransitive (↥G) (Fin 3)] : ∃! j : TransitiveGroupIndex 3, TransitiveGroupLabel j G

A transitive subgroup of the symmetric group on three points carries exactly one label, 3T1 or 3T2.

theorem TauCeti.exists_transitiveGroupLabel_three_iff (G : Subgroup (Equiv.Perm (Fin 3))) : (∃ (j : TransitiveGroupIndex 3), TransitiveGroupLabel j G) ↔ MulAction.IsPretransitive (↥G) (Fin 3)

A subgroup of the symmetric group on three points carries a label exactly when it is transitive.

Degree four

theorem TauCeti.closure_finRotate_four_swap_eq_centralizer : Subgroup.closure {finRotate 4, Equiv.swap 0 2} = Subgroup.centralizer {finRotate 4 ^ 2}

The reference subgroup of 4T3, generated by the rotation of four points and the transposition of two opposite points, is the centralizer of the double transposition finRotate 4 ^ 2.

theorem TauCeti.natCard_referenceSubgroup_four_zero : Nat.card ↥(referenceSubgroup 4 ⟨0, natCard_referenceSubgroup_four_zero._proof_1⟩) = 4

The reference subgroup of 4T1 has order 4.

theorem TauCeti.natCard_referenceSubgroup_four_one : Nat.card ↥(referenceSubgroup 4 ⟨1, natCard_referenceSubgroup_four_one._proof_1⟩) = 4

The reference subgroup of 4T2 has order 4.

theorem TauCeti.natCard_referenceSubgroup_four_two : Nat.card ↥(referenceSubgroup 4 ⟨2, natCard_referenceSubgroup_four_two._proof_1⟩) = 8

The reference subgroup of 4T3 has order 8.

theorem TauCeti.natCard_referenceSubgroup_four_three : Nat.card ↥(referenceSubgroup 4 ⟨3, natCard_referenceSubgroup_four_three._proof_1⟩) = 12

The reference subgroup of 4T4 has order 12.

theorem TauCeti.natCard_referenceSubgroup_four_four : Nat.card ↥(referenceSubgroup 4 ⟨4, natCard_referenceSubgroup_four_four._proof_1⟩) = 24

The reference subgroup of 4T5 has order 24.

theorem TauCeti.not_isCyclic_referenceSubgroup_four_one : ¬IsCyclic ↥(referenceSubgroup 4 ⟨1, natCard_referenceSubgroup_four_one._proof_1⟩)

The reference subgroup of 4T2 is not cyclic: it is the Klein four-group.

theorem TauCeti.not_referenceSubgroup_four_zero_le_alternatingGroup : ¬referenceSubgroup 4 ⟨0, natCard_referenceSubgroup_four_zero._proof_1⟩ ≤ alternatingGroup (Fin 4)

The reference subgroup of 4T1 is not contained in the alternating group: it contains the odd permutation finRotate 4.

theorem TauCeti.referenceSubgroup_four_one_le_alternatingGroup : referenceSubgroup 4 ⟨1, natCard_referenceSubgroup_four_one._proof_1⟩ ≤ alternatingGroup (Fin 4)

The reference subgroup of 4T2 consists of even permutations.

theorem TauCeti.referenceSubgroup_four_zero_le_referenceSubgroup_four_two : referenceSubgroup 4 ⟨0, natCard_referenceSubgroup_four_zero._proof_1⟩ ≤ referenceSubgroup 4 ⟨2, natCard_referenceSubgroup_four_two._proof_1⟩

The reference subgroup of 4T1, the cyclic group of the rotation of four points, lies in that of 4T3.

theorem TauCeti.referenceSubgroup_four_one_le_referenceSubgroup_four_two : referenceSubgroup 4 ⟨1, natCard_referenceSubgroup_four_one._proof_1⟩ ≤ referenceSubgroup 4 ⟨2, natCard_referenceSubgroup_four_two._proof_1⟩

The reference subgroup of 4T2, the Klein four-group, lies in that of 4T3: its nontrivial elements are the three double transpositions, and each of them commutes with the double transposition finRotate 4 ^ 2.

theorem TauCeti.not_referenceSubgroup_four_two_le_alternatingGroup : ¬referenceSubgroup 4 ⟨2, natCard_referenceSubgroup_four_two._proof_1⟩ ≤ alternatingGroup (Fin 4)

The reference subgroup of 4T3 is not contained in the alternating group: it contains the odd permutation finRotate 4.

theorem TauCeti.referenceSubgroup_four_three_le_alternatingGroup : referenceSubgroup 4 ⟨3, natCard_referenceSubgroup_four_three._proof_1⟩ ≤ alternatingGroup (Fin 4)

The reference subgroup of 4T4 consists of even permutations.

theorem TauCeti.not_referenceSubgroup_four_four_le_alternatingGroup : ¬referenceSubgroup 4 ⟨4, natCard_referenceSubgroup_four_four._proof_1⟩ ≤ alternatingGroup (Fin 4)

The reference subgroup of 4T5 is not contained in the alternating group.

theorem TauCeti.referenceSubgroup_four_le_alternatingGroup_iff (j : TransitiveGroupIndex 4) : referenceSubgroup 4 j ≤ alternatingGroup (Fin 4) ↔ ↑j = 1 ∨ ↑j = 3

The parities of the quartic labels. Of the five transitive subgroups of the symmetric group on four points, the Klein four-group of 4T2 and the alternating group of 4T4 consist of even permutations, and the cyclic, dihedral and symmetric groups of 4T1, 4T3 and 4T5 do not.

theorem TauCeti.exists_le_map_conj_referenceSubgroup_four_two_iff (j : TransitiveGroupIndex 4) : (∃ (τ : Equiv.Perm (Fin 4)), referenceSubgroup 4 j ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) (referenceSubgroup 4 ⟨2, natCard_referenceSubgroup_four_two._proof_1⟩)) ↔ ↑j ≤ 2

Which quartic labels a dihedral group of order eight contains. A reference subgroup of degree four lies in a conjugate of the reference subgroup of 4T3 exactly for the labels 4T1, 4T2 and 4T3; the alternating group of 4T4 and the symmetric group of 4T5 have order 12 and 24, which do not divide 8.

theorem TauCeti.TransitiveGroupLabel.eq_of_four {j k : TransitiveGroupIndex 4} {G : Subgroup (Equiv.Perm (Fin 4))} (hj : TransitiveGroupLabel j G) (hk : TransitiveGroupLabel k G) : j = k

A subgroup of the symmetric group on four points carries at most one label.

theorem TauCeti.exists_transitiveGroupLabel_four (G : Subgroup (Equiv.Perm (Fin 4))) [MulAction.IsPretransitive (↥G) (Fin 4)] : ∃ (j : TransitiveGroupIndex 4), TransitiveGroupLabel j G

Every transitive subgroup of the symmetric group on four points carries a label.

theorem TauCeti.existsUnique_transitiveGroupLabel_four (G : Subgroup (Equiv.Perm (Fin 4))) [MulAction.IsPretransitive (↥G) (Fin 4)] : ∃! j : TransitiveGroupIndex 4, TransitiveGroupLabel j G

A transitive subgroup of the symmetric group on four points carries exactly one label, one of 4T1, …, 4T5.

theorem TauCeti.exists_transitiveGroupLabel_four_iff (G : Subgroup (Equiv.Perm (Fin 4))) : (∃ (j : TransitiveGroupIndex 4), TransitiveGroupLabel j G) ↔ MulAction.IsPretransitive (↥G) (Fin 4)

A subgroup of the symmetric group on four points carries a label exactly when it is transitive.

Degree five

theorem TauCeti.transitiveGroupLabelFactPrimeFive : Fact (Nat.Prime 5)

theorem TauCeti.natCard_referenceSubgroup_five_zero : Nat.card ↥(referenceSubgroup 5 ⟨0, natCard_referenceSubgroup_five_zero._proof_1⟩) = 5

The reference subgroup of 5T1 has order 5.

theorem TauCeti.exists_sylow_eq_referenceSubgroup_five_zero : ∃ (P : Sylow 5 (Equiv.Perm (Fin 5))), ↑P = referenceSubgroup 5 ⟨0, natCard_referenceSubgroup_five_zero._proof_1⟩

The reference subgroup of 5T1 is a Sylow 5-subgroup of the symmetric group on five points.

theorem TauCeti.referenceSubgroup_five_zero_le_referenceSubgroup_five_one : referenceSubgroup 5 ⟨0, natCard_referenceSubgroup_five_zero._proof_1⟩ ≤ referenceSubgroup 5 ⟨1, referenceSubgroup_five_zero_le_referenceSubgroup_five_one._proof_1⟩

The reference subgroup of 5T1 lies in that of 5T2.

theorem TauCeti.referenceSubgroup_five_zero_le_referenceSubgroup_five_two : referenceSubgroup 5 ⟨0, natCard_referenceSubgroup_five_zero._proof_1⟩ ≤ referenceSubgroup 5 ⟨2, referenceSubgroup_five_zero_le_referenceSubgroup_five_two._proof_1⟩

The reference subgroup of 5T1 lies in that of 5T3.

theorem TauCeti.referenceSubgroup_five_two_eq_normalizer_referenceSubgroup_five_zero : referenceSubgroup 5 ⟨2, referenceSubgroup_five_zero_le_referenceSubgroup_five_two._proof_1⟩ = Subgroup.normalizer ↑(referenceSubgroup 5 ⟨0, natCard_referenceSubgroup_five_zero._proof_1⟩)

The reference subgroup of 5T3, generated by the rotation i ↦ i + 1 and the affine map i ↦ 2 i + 1 of ℤ/5, is the normalizer of the reference subgroup of 5T1.

theorem TauCeti.natCard_referenceSubgroup_five_two : Nat.card ↥(referenceSubgroup 5 ⟨2, referenceSubgroup_five_zero_le_referenceSubgroup_five_two._proof_1⟩) = 20

The reference subgroup of 5T3 has order 20.

theorem TauCeti.referenceSubgroup_five_one_le_referenceSubgroup_five_two : referenceSubgroup 5 ⟨1, referenceSubgroup_five_zero_le_referenceSubgroup_five_one._proof_1⟩ ≤ referenceSubgroup 5 ⟨2, referenceSubgroup_five_zero_le_referenceSubgroup_five_two._proof_1⟩

The reference subgroup of 5T2 lies in that of 5T3: the double transposition i ↦ 3 - i generating it with the rotation is the square of i ↦ 2 i + 1.

theorem TauCeti.index_referenceSubgroup_five_two : (referenceSubgroup 5 ⟨2, referenceSubgroup_five_zero_le_referenceSubgroup_five_two._proof_1⟩).index = 6

The reference subgroup of 5T3 has index 6.

theorem TauCeti.not_isSwap_of_mem_referenceSubgroup_five_two {σ : Equiv.Perm (Fin 5)} (hσ : σ ∈ referenceSubgroup 5 ⟨2, referenceSubgroup_five_zero_le_referenceSubgroup_five_two._proof_1⟩) : ¬σ.IsSwap

The reference subgroup of 5T3 contains no transposition: a subgroup of Equiv.Perm (Fin 5) whose order is divisible by 5 and which contains a transposition is the whole symmetric group, whereas this one has order 20.

theorem TauCeti.referenceSubgroup_five_one_le_alternatingGroup : referenceSubgroup 5 ⟨1, referenceSubgroup_five_zero_le_referenceSubgroup_five_one._proof_1⟩ ≤ alternatingGroup (Fin 5)

The reference subgroup of 5T2 consists of even permutations.

theorem TauCeti.not_referenceSubgroup_five_two_le_alternatingGroup : ¬referenceSubgroup 5 ⟨2, referenceSubgroup_five_zero_le_referenceSubgroup_five_two._proof_1⟩ ≤ alternatingGroup (Fin 5)

The reference subgroup of 5T3 is not contained in the alternating group: it contains the odd permutation i ↦ 2 i + 1, a four-cycle.

theorem TauCeti.natCard_referenceSubgroup_five_one : Nat.card ↥(referenceSubgroup 5 ⟨1, referenceSubgroup_five_zero_le_referenceSubgroup_five_one._proof_1⟩) = 10

The reference subgroup of 5T2 has order 10.

theorem TauCeti.natCard_referenceSubgroup_five_three : Nat.card ↥(referenceSubgroup 5 ⟨3, natCard_referenceSubgroup_five_three._proof_1⟩) = 60

The reference subgroup of 5T4 has order 60.

theorem TauCeti.natCard_referenceSubgroup_five_four : Nat.card ↥(referenceSubgroup 5 ⟨4, natCard_referenceSubgroup_five_four._proof_1⟩) = 120

The reference subgroup of 5T5 has order 120.

theorem TauCeti.referenceSubgroup_five_zero_le_alternatingGroup : referenceSubgroup 5 ⟨0, natCard_referenceSubgroup_five_zero._proof_1⟩ ≤ alternatingGroup (Fin 5)

The reference subgroup of 5T1, the rotation group, consists of even permutations: it lies in the dihedral group of 5T2.

theorem TauCeti.not_referenceSubgroup_five_four_le_alternatingGroup : ¬referenceSubgroup 5 ⟨4, natCard_referenceSubgroup_five_four._proof_1⟩ ≤ alternatingGroup (Fin 5)

The reference subgroup of 5T5 is not contained in the alternating group: it is the whole symmetric group, which contains the odd permutations of 5T3.

theorem TauCeti.referenceSubgroup_five_le_alternatingGroup_iff (j : TransitiveGroupIndex 5) : referenceSubgroup 5 j ≤ alternatingGroup (Fin 5) ↔ ↑j = 0 ∨ ↑j = 1 ∨ ↑j = 3

The parities of the quintic labels. Of the five transitive subgroups of the symmetric group on five points, the cyclic group of 5T1, the dihedral group of 5T2 and the alternating group of 5T4 consist of even permutations, and the Frobenius group of 5T3 and the symmetric group of 5T5 do not.

theorem TauCeti.TransitiveGroupLabel.eq_of_five {j k : TransitiveGroupIndex 5} {G : Subgroup (Equiv.Perm (Fin 5))} (hj : TransitiveGroupLabel j G) (hk : TransitiveGroupLabel k G) : j = k

A subgroup of the symmetric group on five points carries at most one label.

theorem TauCeti.exists_transitiveGroupLabel_five (G : Subgroup (Equiv.Perm (Fin 5))) [MulAction.IsPretransitive (↥G) (Fin 5)] : ∃ (j : TransitiveGroupIndex 5), TransitiveGroupLabel j G

Every transitive subgroup of the symmetric group on five points carries a label.

theorem TauCeti.existsUnique_transitiveGroupLabel_five (G : Subgroup (Equiv.Perm (Fin 5))) [MulAction.IsPretransitive (↥G) (Fin 5)] : ∃! j : TransitiveGroupIndex 5, TransitiveGroupLabel j G

A transitive subgroup of the symmetric group on five points carries exactly one label, one of 5T1, …, 5T5.

theorem TauCeti.exists_transitiveGroupLabel_five_iff (G : Subgroup (Equiv.Perm (Fin 5))) : (∃ (j : TransitiveGroupIndex 5), TransitiveGroupLabel j G) ↔ MulAction.IsPretransitive (↥G) (Fin 5)

A subgroup of the symmetric group on five points carries a label exactly when it is transitive.