Primitivity of the transitive groups of degree at most five

The reference subgroups TauCeti.referenceSubgroup represent the transitive subgroups of the symmetric groups on at most five points. This file determines which of them act primitively.

In prime degree every transitive group is primitive, which settles the degrees two, three and five, and the one-point action of degree one is primitive by Mathlib's convention. In degree four, the alternating group 4T4 and the symmetric group 4T5 are primitive, while the cyclic group 4T1, the Klein four-group 4T2 and the dihedral group 4T3 are not: the dihedral group of order eight is the image of the imprimitive wreath product C₂ ≀ S₂, which preserves a partition of the four points into two pairs, and the other two groups lie inside it.

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

Main results

• TauCeti.isPreprimitive_referenceSubgroup_of_prime: in prime degree every reference subgroup is primitive.
• TauCeti.not_isPreprimitive_referenceSubgroup_four_two, with its companions for 4T1 and 4T2: the three imprimitive quartic labels.
• TauCeti.isPreprimitive_referenceSubgroup_four_iff: in degree four exactly 4T4 and 4T5 are primitive.
• TauCeti.isPreprimitive_referenceSubgroup_iff: the primitivity column of the table of transitive groups of degree at most five.
• TauCeti.TransitiveGroupLabel.isPreprimitive_iff_ne_four_or_three_le: a permutation group with a label is primitive exactly when its label is not 4T1, 4T2 or 4T3.

theorem TauCeti.isPreprimitive_referenceSubgroup_one (j : TransitiveGroupIndex 1) : MulAction.IsPreprimitive (↥(referenceSubgroup 1 j)) (Fin 1)

In degree one the unique reference subgroup acts primitively on the single point.

theorem TauCeti.isPreprimitive_referenceSubgroup_of_prime {n : ℕ} (hn : Nat.Prime n) (j : TransitiveGroupIndex n) : MulAction.IsPreprimitive (↥(referenceSubgroup n j)) (Fin n)

In prime degree every reference subgroup is primitive, being transitive on a set of prime cardinality.

theorem TauCeti.not_isPreprimitive_referenceSubgroup_four_two : ¬MulAction.IsPreprimitive (↥(referenceSubgroup 4 ⟨2, not_isPreprimitive_referenceSubgroup_four_two._proof_1⟩)) (Fin 4)

The reference subgroup of 4T3, the dihedral group of order eight, is not primitive: it is conjugate to the image of the imprimitive wreath product C₂ ≀ S₂, which preserves a partition of the four points into two pairs.

theorem TauCeti.not_isPreprimitive_referenceSubgroup_four_zero : ¬MulAction.IsPreprimitive (↥(referenceSubgroup 4 ⟨0, not_isPreprimitive_referenceSubgroup_four_zero._proof_1⟩)) (Fin 4)

The reference subgroup of 4T1, the cyclic group of order four, is not primitive: it lies in the dihedral group of 4T3.

theorem TauCeti.not_isPreprimitive_referenceSubgroup_four_one : ¬MulAction.IsPreprimitive (↥(referenceSubgroup 4 ⟨1, not_isPreprimitive_referenceSubgroup_four_one._proof_1⟩)) (Fin 4)

The reference subgroup of 4T2, the Klein four-group, is not primitive: it lies in the dihedral group of 4T3.

theorem TauCeti.isPreprimitive_referenceSubgroup_four_three : MulAction.IsPreprimitive (↥(referenceSubgroup 4 ⟨3, isPreprimitive_referenceSubgroup_four_three._proof_1⟩)) (Fin 4)

The reference subgroup of 4T4, the alternating group, is primitive.

theorem TauCeti.isPreprimitive_referenceSubgroup_four_four : MulAction.IsPreprimitive (↥(referenceSubgroup 4 ⟨4, isPreprimitive_referenceSubgroup_four_four._proof_1⟩)) (Fin 4)

The reference subgroup of 4T5, the symmetric group, is primitive.

theorem TauCeti.isPreprimitive_referenceSubgroup_four_iff (j : TransitiveGroupIndex 4) : MulAction.IsPreprimitive (↥(referenceSubgroup 4 j)) (Fin 4) ↔ 3 ≤ ↑j

The primitive quartic labels. Of the five transitive subgroups of the symmetric group on four points, the alternating group of 4T4 and the symmetric group of 4T5 are primitive, and the cyclic, Klein four and dihedral groups of 4T1, 4T2 and 4T3 are not.

@[simp]

theorem TauCeti.isPreprimitive_referenceSubgroup_iff {n : ℕ} (j : TransitiveGroupIndex n) : MulAction.IsPreprimitive (↥(referenceSubgroup n j)) (Fin n) ↔ n ≠ 4 ∨ 3 ≤ ↑j

The primitivity column of the table of transitive groups of degree at most five. A reference subgroup acts primitively unless its label is one of 4T1, 4T2 and 4T3.

theorem TauCeti.TransitiveGroupLabel.isPreprimitive_iff_ne_four_or_three_le {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : MulAction.IsPreprimitive (↥G) (Fin n) ↔ n ≠ 4 ∨ 3 ≤ ↑j

A permutation group with a transitive-group label acts primitively exactly when its label is not one of 4T1, 4T2 and 4T3.