Recognition of the low-degree transitive groups by order

In degrees at most five, the order of a transitive permutation group determines its transitive-group label up to one collision: the two labels of order four, 4T1 and 4T2, are distinguished by cyclicity. Together with TauCeti.TransitiveGroupLabel.isCyclic_iff, which transports cyclicity across a transitive-group label, this recognizes every label of degree at most five from the order of the labelled subgroup alone, or from its order and cyclicity in degree four.

Main results

• TauCeti.TransitiveGroupLabel.natCard_mem_three, TauCeti.TransitiveGroupLabel.natCard_mem_four: the order of a subgroup labelled 3Tj or 4Tj is one of 3, 6 or 4, 8, 12, 24, respectively. In degree five the corresponding fact follows from TauCeti.natCard_mem_of_natCard_eq_five_of_isPretransitive and TauCeti.TransitiveGroupLabel.isPretransitive.
• TauCeti.transitiveGroupLabel_three_iff_natCard_eq, TauCeti.transitiveGroupLabel_five_iff_natCard_eq: in degrees three and five the order recognizes the label.
• TauCeti.transitiveGroupLabel_four_zero_iff, TauCeti.transitiveGroupLabel_four_one_iff: the two labels of order four in degree four are exactly distinguished by cyclicity.
• TauCeti.transitiveGroupLabel_four_one_iff_isKleinFour: a transitive subgroup of S₄ has label 4T2 exactly when it is a Klein four-group.
• TauCeti.transitiveGroupLabel_four_iff_natCard_eq_of_two_le: the order recognizes the labels 4T3, 4T4 and 4T5.

Tags

transitive group, recognition, order

theorem TauCeti.TransitiveGroupLabel.natCard_mem_three {j : TransitiveGroupIndex 3} {G : Subgroup (Equiv.Perm (Fin 3))} (h : TransitiveGroupLabel j G) : Nat.card ↥G ∈ {3, 6}

The order of a labelled subgroup of S₃ is 3 or 6. These are the orders 3, 6 of the labels 3T1 and 3T2.

theorem TauCeti.TransitiveGroupLabel.natCard_mem_four {j : TransitiveGroupIndex 4} {G : Subgroup (Equiv.Perm (Fin 4))} (h : TransitiveGroupLabel j G) : Nat.card ↥G ∈ {4, 8, 12, 24}

The order of a labelled subgroup of S₄ is one of 4, 8, 12, 24. These are the orders 4, 4, 8, 12, 24 of the labels 4T1 through 4T5; the two labels of order four give the single value 4.

@[simp]

theorem TauCeti.transitiveGroupLabel_three_iff_natCard_eq (j : TransitiveGroupIndex 3) (G : Subgroup (Equiv.Perm (Fin 3))) [MulAction.IsPretransitive (↥G) (Fin 3)] : TransitiveGroupLabel j G ↔ Nat.card ↥G = Nat.card ↥(referenceSubgroup 3 j)

Order recognition in degree three. A transitive subgroup of S₃ is labelled 3Tj exactly when its order is that of 3Tj: the orders 3, 6 of 3T1 and 3T2 are distinct.

@[simp]

theorem TauCeti.transitiveGroupLabel_five_iff_natCard_eq (j : TransitiveGroupIndex 5) (G : Subgroup (Equiv.Perm (Fin 5))) [MulAction.IsPretransitive (↥G) (Fin 5)] : TransitiveGroupLabel j G ↔ Nat.card ↥G = Nat.card ↥(referenceSubgroup 5 j)

Order recognition in degree five. A transitive subgroup of S₅ is labelled 5Tj exactly when its order is that of 5Tj: the orders 5, 10, 20, 60, 120 of 5T1 through 5T5 are pairwise distinct.

@[simp]

theorem TauCeti.transitiveGroupLabel_four_zero_iff (G : Subgroup (Equiv.Perm (Fin 4))) [MulAction.IsPretransitive (↥G) (Fin 4)] : TransitiveGroupLabel ⟨0, transitiveGroupLabel_four_zero_iff._proof_1⟩ G ↔ Nat.card ↥G = 4 ∧ IsCyclic ↥G

4T1 is recognized by its order and cyclicity. A transitive subgroup of S₄ is labelled 4T1 exactly when it has order four and is cyclic. The hypothesis IsCyclic G cannot be dropped: 4T2 also has order four.

@[simp]

theorem TauCeti.transitiveGroupLabel_four_one_iff (G : Subgroup (Equiv.Perm (Fin 4))) [MulAction.IsPretransitive (↥G) (Fin 4)] : TransitiveGroupLabel ⟨1, transitiveGroupLabel_four_one_iff._proof_1⟩ G ↔ Nat.card ↥G = 4 ∧ ¬IsCyclic ↥G

4T2 is recognized by its order and non-cyclicity. A transitive subgroup of S₄ is labelled 4T2 exactly when it has order four and is not cyclic, that is, exactly when it is a Klein four-group up to conjugacy.

theorem TauCeti.transitiveGroupLabel_four_one_iff_isKleinFour (G : Subgroup (Equiv.Perm (Fin 4))) [MulAction.IsPretransitive (↥G) (Fin 4)] : TransitiveGroupLabel ⟨1, transitiveGroupLabel_four_one_iff._proof_1⟩ G ↔ IsKleinFour ↥G

4T2 is recognized as the Klein four-group. A transitive subgroup of S₄ has label 4T2 exactly when it is a Klein four-group.

@[simp]

theorem TauCeti.transitiveGroupLabel_four_iff_natCard_eq_of_two_le (j : TransitiveGroupIndex 4) (hj : 2 ≤ ↑j) (G : Subgroup (Equiv.Perm (Fin 4))) [MulAction.IsPretransitive (↥G) (Fin 4)] : TransitiveGroupLabel j G ↔ Nat.card ↥G = Nat.card ↥(referenceSubgroup 4 j)

Order recognition in degree four away from order four. A transitive subgroup of S₄ is labelled 4Tj, 2 ≤ j, exactly when its order is that of 4Tj: the orders 8, 12, 24 of 4T3, 4T4 and 4T5 are pairwise distinct and differ from the order four of 4T1 and 4T2.