Parity of the transitive groups of degree at most five

The reference groups consisting entirely of even permutations are exactly 1T1, 3T1, 4T2, 4T4, 5T1, 5T2, and 5T4. The theorem TauCeti.referenceSubgroup_le_alternatingGroup_iff gives this complete list, using zero-based label indices. Its counterpart for TauCeti.TransitiveGroupLabel reads the same list for any labelled subgroup, since parity is invariant under conjugation.

Together with the discriminant test, this list determines which polynomial labels have square discriminant away from characteristic two.

References

• LMFDB, Galois group labels, https://www.lmfdb.org/GaloisGroup/.

@[simp]

theorem TauCeti.referenceSubgroup_le_alternatingGroup_iff {n : ℕ} (j : TransitiveGroupIndex n) : referenceSubgroup n j ≤ alternatingGroup (Fin n) ↔ n = 1 ∨ n = 3 ∧ ↑j = 0 ∨ n = 4 ∧ (↑j = 1 ∨ ↑j = 3) ∨ n = 5 ∧ (↑j = 0 ∨ ↑j = 1 ∨ ↑j = 3)

The parity column of the transitive groups of degree at most five. The reference subgroup consists of even permutations exactly for the labels 1T1, 3T1, 4T2, 4T4, 5T1, 5T2, and 5T4. The label index is zero-based.

theorem TauCeti.TransitiveGroupLabel.le_alternatingGroup_iff_label {n : ℕ} {j : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))} (h : TransitiveGroupLabel j G) : G ≤ alternatingGroup (Fin n) ↔ n = 1 ∨ n = 3 ∧ ↑j = 0 ∨ n = 4 ∧ (↑j = 1 ∨ ↑j = 3) ∨ n = 5 ∧ (↑j = 0 ∨ ↑j = 1 ∨ ↑j = 3)

A labelled subgroup consists of even permutations exactly for the labels 1T1, 3T1, 4T2, 4T4, 5T1, 5T2, and 5T4.