Reference transitive permutation groups in degree at most five

This file defines the reference permutation groups underlying the standard nTj labels in degrees at most five. A label records the ambient conjugacy class of a subgroup of the symmetric group; it does not attach an abstract group name or classify arbitrary subgroups.

The chosen generators are the zero-based translations of the representatives in the LMFDB transitive-groups table. The reference family is empty outside degrees one through five.

Main definitions

• numTransitiveGroups: the number of reference groups in each supported degree.
• TransitiveGroupIndex: the type of valid zero-based label indices.
• referenceSubgroup: the subgroup represented by a valid index.
• TransitiveGroupLabel: conjugacy to a reference subgroup.

Main results

• TauCeti.isPretransitive_referenceSubgroup: every reference subgroup is transitive.
• Subgroup.transitiveGroupLabel_map_permCongrHom_iff: the label of a permutation group on an arbitrary set of n points does not depend on the numbering by Fin n used to read it.
• TauCeti.TransitiveGroupLabel.exists_le_map_conj_of_le: inclusion of a reference subgroup in a larger subgroup transports to inclusion of the labelled subgroup in a conjugate, and TauCeti.TransitiveGroupLabel.exists_le_map_conj_iff: a labelled subgroup lies in a conjugate of a fixed subgroup exactly when its reference subgroup does.
• TauCeti.TransitiveGroupLabel.natCard_eq, TauCeti.TransitiveGroupLabel.le_alternatingGroup_iff, TauCeti.TransitiveGroupLabel.isPretransitive_inf_alternatingGroup_iff, TauCeti.TransitiveGroupLabel.isPreprimitive_iff, TauCeti.TransitiveGroupLabel.isSolvable_iff, TauCeti.TransitiveGroupLabel.isCyclic_iff: a labelled subgroup has the order, parity, even-part transitivity, primitivity, solvability, and cyclicity of its reference.
• TauCeti.transitiveGroupLabel_one, TauCeti.transitiveGroupLabel_two_iff: in degrees one and two, a subgroup carries the unique label exactly when it is transitive.

References

• LMFDB, Transitive groups, entries of degrees at most five.
• G. Butler and J. McKay, The transitive groups of degree up to eleven.

def TauCeti.numTransitiveGroups : ℕ → ℕ

The number of reference transitive permutation groups in a supported degree.

The supported values are 1, 1, 2, 5, 5 in degrees one through five, and zero in every other degree.

Equations

• TauCeti.numTransitiveGroups 1 = 1
• TauCeti.numTransitiveGroups 2 = 1
• TauCeti.numTransitiveGroups 3 = 2
• TauCeti.numTransitiveGroups 4 = 5
• TauCeti.numTransitiveGroups 5 = 5
• TauCeti.numTransitiveGroups x✝ = 0

@[simp]

theorem TauCeti.numTransitiveGroups_zero : numTransitiveGroups 0 = 0

@[simp]

theorem TauCeti.numTransitiveGroups_one : numTransitiveGroups 1 = 1

@[simp]

theorem TauCeti.numTransitiveGroups_two : numTransitiveGroups 2 = 1

@[simp]

theorem TauCeti.numTransitiveGroups_three : numTransitiveGroups 3 = 2

@[simp]

theorem TauCeti.numTransitiveGroups_four : numTransitiveGroups 4 = 5

There are five reference groups in degree four.

@[simp]

theorem TauCeti.numTransitiveGroups_five : numTransitiveGroups 5 = 5

@[simp]

theorem TauCeti.numTransitiveGroups_eq_zero_of_five_lt {n : ℕ} (hn : 5 < n) : numTransitiveGroups n = 0

There are no reference groups in degree greater than five.

@[reducible, inline]

abbrev TauCeti.TransitiveGroupIndex (n : ℕ) : Type

A zero-based index for a transitive-group label in degree n.

An index j is displayed externally as nT(j + 1).

Equations

• TauCeti.TransitiveGroupIndex n = Fin (TauCeti.numTransitiveGroups n)

theorem TauCeti.pos_of_transitiveGroupIndex {n : ℕ} (j : TransitiveGroupIndex n) : 0 < n

There are no labels in degree zero, so a label index has a positive degree.

def TauCeti.referenceSubgroup (n : ℕ) : TransitiveGroupIndex n → Subgroup (Equiv.Perm (Fin n))

The reference subgroup represented by a transitive-group label of degree at most five.

The entries use the standard ordering 1T1, 2T1, 3T1--3T2, 4T1--4T5, and 5T1--5T5.

Equations

• TauCeti.referenceSubgroup 0 = Fin.elim0
• TauCeti.referenceSubgroup 1 = fun (x : TauCeti.TransitiveGroupIndex 1) => ⊤
• TauCeti.referenceSubgroup 2 = fun (x : TauCeti.TransitiveGroupIndex 2) => ⊤
• TauCeti.referenceSubgroup 3 = TauCeti.referenceSubgroup3✝
• TauCeti.referenceSubgroup 4 = TauCeti.referenceSubgroup4✝
• TauCeti.referenceSubgroup 5 = TauCeti.referenceSubgroup5✝
• TauCeti.referenceSubgroup n_2.succ.succ.succ.succ.succ.succ = Fin.elim0

def TauCeti.TransitiveGroupLabel {n : ℕ} (j : TransitiveGroupIndex n) (G : Subgroup (Equiv.Perm (Fin n))) : Prop

A subgroup has label j when it is conjugate in the ambient symmetric group to the corresponding reference subgroup.

Equations

• TauCeti.TransitiveGroupLabel j G = ∃ (τ : Equiv.Perm (Fin n)), Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) G = TauCeti.referenceSubgroup n j

theorem TauCeti.transitiveGroupLabel_iff {n : ℕ} (j : TransitiveGroupIndex n) (G : Subgroup (Equiv.Perm (Fin n))) : TransitiveGroupLabel j G ↔ ∃ (τ : Equiv.Perm (Fin n)), Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) G = referenceSubgroup n j

A transitive-group label is equivalent to the existence of a conjugating permutation.

@[simp]

theorem TauCeti.referenceSubgroup_one (j : TransitiveGroupIndex 1) : referenceSubgroup 1 j = ⊤

The reference subgroup for 1T1 is the full symmetric group on one letter.

@[simp]

theorem TauCeti.referenceSubgroup_two (j : TransitiveGroupIndex 2) : referenceSubgroup 2 j = ⊤

The reference subgroup for 2T1 is the full symmetric group on two letters.

@[simp]

theorem TauCeti.referenceSubgroup_three_zero : referenceSubgroup 3 ⟨0, referenceSubgroup_three_zero._proof_8⟩ = Subgroup.closure {finRotate 3}

The reference subgroup for 3T1 is generated by a rotation.

@[simp]

theorem TauCeti.referenceSubgroup_three_one : referenceSubgroup 3 ⟨1, referenceSubgroup_three_one._proof_1⟩ = ⊤

The reference subgroup for 3T2 is the full symmetric group.

@[simp]

theorem TauCeti.referenceSubgroup_four_zero : referenceSubgroup 4 ⟨0, referenceSubgroup_four_zero._proof_1⟩ = Subgroup.closure {finRotate 4}

The reference subgroup for 4T1 is generated by a rotation.

@[simp]

theorem TauCeti.referenceSubgroup_four_one : referenceSubgroup 4 ⟨1, referenceSubgroup_four_one._proof_1⟩ = Subgroup.map (alternatingGroup (Fin 4)).subtype (alternatingGroup.kleinFour (Fin 4))

The reference subgroup for 4T2 is the canonical Klein-four subgroup.

@[simp]

theorem TauCeti.referenceSubgroup_four_two : referenceSubgroup 4 ⟨2, referenceSubgroup_four_two._proof_1⟩ = Subgroup.closure {finRotate 4, Equiv.swap 0 2}

The reference subgroup for 4T3 is generated by a rotation and a diagonal swap.

theorem TauCeti.mem_referenceSubgroup_four_two_iff {σ : Equiv.Perm (Fin 4)} : σ ∈ referenceSubgroup 4 ⟨2, referenceSubgroup_four_two._proof_1⟩ ↔ ∀ (i : Fin 4), σ (i + 2) = σ i + 2

The reference subgroup for 4T3 is the dihedral group of the square 0, 1, 2, 3: a permutation lies in it exactly when it preserves the pairing {{0, 2}, {1, 3}} of opposite vertices, that is, commutes with i ↦ i + 2.

@[simp]

theorem TauCeti.referenceSubgroup_four_three : referenceSubgroup 4 ⟨3, referenceSubgroup_four_three._proof_1⟩ = alternatingGroup (Fin 4)

The reference subgroup for 4T4 is the alternating group.

@[simp]

theorem TauCeti.referenceSubgroup_four_four : referenceSubgroup 4 ⟨4, referenceSubgroup_four_four._proof_1⟩ = ⊤

The reference subgroup for 4T5 is the full symmetric group.

@[simp]

theorem TauCeti.referenceSubgroup_five_zero : referenceSubgroup 5 ⟨0, referenceSubgroup_five_zero._proof_1⟩ = Subgroup.closure {finRotate 5}

The reference subgroup for 5T1 is generated by a rotation.

@[simp]

theorem TauCeti.referenceSubgroup_five_one : referenceSubgroup 5 ⟨1, referenceSubgroup_five_one._proof_1⟩ = Subgroup.closure {finRotate 5, Equiv.swap 0 3 * Equiv.swap 1 2}

The reference subgroup for 5T2 is generated by a rotation and a double swap.

@[simp]

theorem TauCeti.referenceSubgroup_five_two : referenceSubgroup 5 ⟨2, referenceSubgroup_five_two._proof_1⟩ = Subgroup.closure {finRotate 5, [0, 1, 3, 2].formPerm}

The reference subgroup for 5T3 is generated by a rotation and a Frobenius complement.

@[simp]

theorem TauCeti.referenceSubgroup_five_three : referenceSubgroup 5 ⟨3, referenceSubgroup_five_three._proof_1⟩ = alternatingGroup (Fin 5)

The reference subgroup for 5T4 is the alternating group.

@[simp]

theorem TauCeti.referenceSubgroup_five_four : referenceSubgroup 5 ⟨4, referenceSubgroup_five_four._proof_1⟩ = ⊤

The reference subgroup for 5T5 is the full symmetric group.

theorem TauCeti.isPretransitive_referenceSubgroup (n : ℕ) (j : TransitiveGroupIndex n) : MulAction.IsPretransitive (↥(referenceSubgroup n j)) (Fin n)

Every reference subgroup acts transitively in its defining permutation representation.

@[simp]

theorem TauCeti.transitiveGroupLabel_referenceSubgroup (n : ℕ) (j : TransitiveGroupIndex n) : TransitiveGroupLabel j (referenceSubgroup n j)

A reference subgroup carries its defining transitive-group label.

theorem TauCeti.TransitiveGroupLabel.map_conj {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) (σ : Equiv.Perm (Fin n)) : TransitiveGroupLabel j (Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj σ)) G)

Conjugating the permutation representation does not change its transitive-group label.

@[simp]

theorem TauCeti.transitiveGroupLabel_map_conj_iff {n : ℕ} {j : TransitiveGroupIndex n} (G : Subgroup (Equiv.Perm (Fin n))) (σ : Equiv.Perm (Fin n)) : TransitiveGroupLabel j (Subgroup.map (↑(MulAut.conj σ)) G) ↔ TransitiveGroupLabel j G

A subgroup and any conjugate subgroup have exactly the same transitive-group labels.

theorem TauCeti.TransitiveGroupLabel.isPretransitive {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : MulAction.IsPretransitive (↥G) (Fin n)

A subgroup carrying a transitive-group label acts transitively on its permutation domain.

theorem TauCeti.TransitiveGroupLabel.exists_map_permCongrHom_eq {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : ∃ (τ : Equiv.Perm (Fin n)), Subgroup.map (Equiv.permCongrHom τ).toMonoidHom G = referenceSubgroup n j

A label is witnessed by a transport of the subgroup along a renumbering of Fin n.

theorem TauCeti.TransitiveGroupLabel.nonempty_mulEquiv_referenceSubgroup {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : Nonempty (↥G ≃* ↥(referenceSubgroup n j))

A subgroup carrying a label is abstractly isomorphic to its reference subgroup.

theorem TauCeti.TransitiveGroupLabel.exists_le_map_conj_of_le {n : ℕ} {j : TransitiveGroupIndex n} {G H : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) (hle : referenceSubgroup n j ≤ H) : ∃ (τ : Equiv.Perm (Fin n)), G ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) H

If a subgroup carries the label j and the reference subgroup for j lies in H, then the subgroup lies in a conjugate of H.

theorem TauCeti.TransitiveGroupLabel.exists_le_map_conj_iff {n : ℕ} {j : TransitiveGroupIndex n} {G H : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : (∃ (τ : Equiv.Perm (Fin n)), G ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) H) ↔ ∃ (τ : Equiv.Perm (Fin n)), referenceSubgroup n j ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) H

Conjugating into a subgroup depends only on the label. A subgroup with the label j lies in a conjugate of H exactly when the reference subgroup of j does. This is what lets a criterion that confines a permutation group to a conjugate of a fixed subgroup, such as the existence of a root of a resolvent, be read as a condition on the label.

theorem Subgroup.transitiveGroupLabel_map_permCongrHom_iff {α : Type u_1} {n : ℕ} {j : TauCeti.TransitiveGroupIndex n} (G : Subgroup (Equiv.Perm α)) (e e' : α ≃ Fin n) : TauCeti.TransitiveGroupLabel j (map e.permCongrHom.toMonoidHom G) ↔ TauCeti.TransitiveGroupLabel j (map e'.permCongrHom.toMonoidHom G)

Reading a permutation group on n points through two numberings by Fin n gives the same transitive-group labels.

theorem TauCeti.TransitiveGroupLabel.natCard_eq {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : Nat.card ↥G = Nat.card ↥(referenceSubgroup n j)

A subgroup carrying a transitive-group label has the order of its reference subgroup.

theorem TauCeti.TransitiveGroupLabel.le_alternatingGroup_iff {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : G ≤ alternatingGroup (Fin n) ↔ referenceSubgroup n j ≤ alternatingGroup (Fin n)

A subgroup carrying a transitive-group label consists of even permutations exactly when its reference subgroup does.

theorem TauCeti.TransitiveGroupLabel.isPretransitive_inf_alternatingGroup_iff {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : MulAction.IsPretransitive (↥(G ⊓ alternatingGroup (Fin n))) (Fin n) ↔ MulAction.IsPretransitive (↥(referenceSubgroup n j ⊓ alternatingGroup (Fin n))) (Fin n)

The even part of a labelled subgroup is transitive exactly when the even part of its reference subgroup is transitive.

theorem TauCeti.TransitiveGroupLabel.isPreprimitive_iff {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : MulAction.IsPreprimitive (↥G) (Fin n) ↔ MulAction.IsPreprimitive (↥(referenceSubgroup n j)) (Fin n)

A subgroup carrying a transitive-group label acts primitively exactly when its reference subgroup does.

theorem TauCeti.TransitiveGroupLabel.isSolvable_iff {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : Group.IsSolvable ↥G ↔ Group.IsSolvable ↥(referenceSubgroup n j)

A subgroup carrying a transitive-group label is solvable exactly when its reference subgroup is.

theorem TauCeti.TransitiveGroupLabel.isCyclic_iff {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : IsCyclic ↥G ↔ IsCyclic ↥(referenceSubgroup n j)

A subgroup carrying a transitive-group label is cyclic exactly when its reference subgroup is.

@[simp]

theorem TauCeti.transitiveGroupLabel_one (j : TransitiveGroupIndex 1) (G : Subgroup (Equiv.Perm (Fin 1))) : TransitiveGroupLabel j G

In degree one every subgroup carries the label 1T1.

@[simp]

theorem TauCeti.transitiveGroupLabel_two_iff (j : TransitiveGroupIndex 2) (G : Subgroup (Equiv.Perm (Fin 2))) : TransitiveGroupLabel j G ↔ MulAction.IsPretransitive (↥G) (Fin 2)

In degree two a subgroup carries the label 2T1 exactly when it is transitive: the only transitive subgroup of the symmetric group on two letters is the whole group.