The transitive-group label of a polynomial

A separable polynomial f of degree n over a field F has n distinct roots in its splitting field, and its Galois group acts faithfully on them. Choosing a numbering e : f.rootSet f.SplittingField ≃ Fin n turns the image of that action into a subgroup of Equiv.Perm (Fin n), which can then be compared with the reference subgroups of TauCeti.referenceSubgroup. The predicate TauCeti.HasGaloisLabel f j says that some numbering carries the Galois image to a subgroup with the label j, that is, onto a conjugate of the reference subgroup referenceSubgroup n j. This is the label nT(j+1) that the LMFDB attaches to f.

The numbering is only a device for the comparison. The main result TauCeti.hasGaloisLabel_iff_forall shows that the label does not depend on it: if one numbering exhibits the label then every numbering does. The predicate is therefore a property of f.

A label records the permutation invariants of the Galois group. f.Gal has the order of the reference subgroup, and it is solvable, respectively acts primitively on the roots, exactly when the reference subgroup is solvable, respectively primitive. The Galois image consists of even permutations exactly when the reference subgroup does, and so, away from characteristic 2 and for monic f, the discriminant of f is a square exactly when the reference subgroup lies in the alternating group. In the same way f stays irreducible over its discriminant field exactly when the even part of the reference subgroup is transitive. Since every reference subgroup is transitive, a polynomial with a label is irreducible.

Separability and the degree are part of the predicate, so an inseparable polynomial, or one of degree other than n, has no label in degree n; nor does a polynomial of degree zero or of degree above five, where there are no reference subgroups. In degree one the label is determined by the degree alone, and in degree two by separability and irreducibility.

Main definitions

• TauCeti.HasGaloisLabel: the Galois image of f, read through some numbering of the roots, carries a given transitive-group label.

Main results

• TauCeti.hasGaloisLabel_iff_forall: the label does not depend on the numbering of the roots.
• TauCeti.HasGaloisLabel.natCard_gal: the order of the Galois group is that of the reference, and TauCeti.hasGaloisLabel_iff_natCard_gal: conversely, the order determines the label in every degree where it determines the label of a transitive subgroup.
• TauCeti.HasGaloisLabel.range_le_alternatingGroup_iff and TauCeti.HasGaloisLabel.isSquare_discr_iff: the parity of the Galois image.
• TauCeti.HasGaloisLabel.range_le_alternatingGroup_iff_label and TauCeti.HasGaloisLabel.isSquare_discr_iff_label: the complete parity column, read as explicit conditions on the degree and label index.
• TauCeti.HasGaloisLabel.irreducible_map_discrField_iff: irreducibility over the discriminant field, read on the even part of the reference subgroup.
• TauCeti.HasGaloisLabel.isPreprimitive_iff, TauCeti.HasGaloisLabel.isPreprimitive_gal_iff: primitivity of the Galois image, respectively of the Galois group, on the roots, and TauCeti.HasGaloisLabel.isPreprimitive_gal_iff_ne_four_or_three_le: the Galois group acts primitively unless the label is 4T1, 4T2 or 4T3.
• TauCeti.HasGaloisLabel.isSolvable_iff: solvability of the Galois group.
• TauCeti.HasGaloisLabel.isSolvable_iff_ne_five_or_lt_three: the Galois group of a polynomial with a label is solvable unless the label is 5T4 or 5T5.
• TauCeti.HasGaloisLabel.eq_one_of_smul_eq_self: a regular label acts freely on the roots.
• TauCeti.HasGaloisLabel.irreducible: a polynomial with a label is irreducible, and TauCeti.exists_hasGaloisLabel_of_irreducible: conversely, an irreducible separable polynomial has a label in every degree where each transitive subgroup has one.
• TauCeti.HasGaloisLabel.eq_of and TauCeti.existsUnique_hasGaloisLabel: uniqueness of the label, in every degree where a subgroup carries at most one.
• TauCeti.hasGaloisLabel_one_iff, TauCeti.hasGaloisLabel_two_iff: the labels in degrees one and two.

References

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

theorem TauCeti.factSplitsSplittingField {F : Type u} [Field F] (f : Polynomial F) : Fact (Polynomial.map (algebraMap F f.SplittingField) f).Splits

A polynomial splits in its splitting field, recorded as the Fact that Polynomial.Gal.galActionHom asks for. It stays local: as a global instance it would give f.rootSet f.SplittingField the action Polynomial.Gal.galAction in addition to Mathlib's intrinsic Polynomial.Gal.galActionAux, and the two are different actions.

def TauCeti.HasGaloisLabel {F : Type u} [Field F] (f : Polynomial F) {n : ℕ} (j : TransitiveGroupIndex n) : Prop

The Galois group of f carries the transitive-group label j of degree n: f is separable of degree n, and some numbering of its roots in the splitting field by Fin n carries the image of the Galois action on the roots to a conjugate of the reference subgroup referenceSubgroup n j. By TauCeti.hasGaloisLabel_iff_forall, every numbering then does.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.isPretransitive_map_range_galActionHom_iff {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} (hsep : f.Separable) (hdeg : 0 < f.natDegree) (e : ↑(f.rootSet f.SplittingField) ≃ Fin n) : MulAction.IsPretransitive (↥(Subgroup.map e.permCongrHom.toMonoidHom (Polynomial.Gal.galActionHom f f.SplittingField).range)) (Fin n) ↔ Irreducible f

The Galois image of a separable polynomial of positive degree, read through any numbering of its roots, is transitive exactly when the polynomial is irreducible.

theorem TauCeti.HasGaloisLabel.mk {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (hsep : f.Separable) (hdeg : f.natDegree = n) (e : ↑(f.rootSet f.SplittingField) ≃ Fin n) (he : TransitiveGroupLabel j (Subgroup.map e.permCongrHom.toMonoidHom (Polynomial.Gal.galActionHom f f.SplittingField).range)) : HasGaloisLabel f j

Construct a Galois label from one numbering of the roots that exhibits it.

theorem TauCeti.HasGaloisLabel.separable {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : f.Separable

A polynomial with a label is separable.

theorem TauCeti.HasGaloisLabel.natDegree_eq {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : f.natDegree = n

A polynomial with a label in degree n has degree n.

theorem TauCeti.HasGaloisLabel.transitiveGroupLabel {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) (e : ↑(f.rootSet f.SplittingField) ≃ Fin n) : TransitiveGroupLabel j (Subgroup.map e.permCongrHom.toMonoidHom (Polynomial.Gal.galActionHom f f.SplittingField).range)

A label is exhibited by every numbering of the roots.

theorem TauCeti.hasGaloisLabel_iff_forall {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} : HasGaloisLabel f j ↔ f.Separable ∧ f.natDegree = n ∧ ∀ (e : ↑(f.rootSet f.SplittingField) ≃ Fin n), TransitiveGroupLabel j (Subgroup.map e.permCongrHom.toMonoidHom (Polynomial.Gal.galActionHom f f.SplittingField).range)

The label does not depend on the numbering of the roots. A separable polynomial of degree n has the label j exactly when every numbering of its roots by Fin n carries its Galois image to a subgroup with the label j.

theorem TauCeti.not_hasGaloisLabel_of_not_separable {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (hf : ¬f.Separable) : ¬HasGaloisLabel f j

An inseparable polynomial has no label.

theorem TauCeti.not_hasGaloisLabel_of_natDegree_ne {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (hf : f.natDegree ≠ n) : ¬HasGaloisLabel f j

A polynomial has no label in a degree other than its own.

theorem TauCeti.HasGaloisLabel.natCard_gal {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : Nat.card f.Gal = Nat.card ↥(referenceSubgroup n j)

The Galois group of a polynomial with a label has the order of the reference subgroup.

theorem TauCeti.HasGaloisLabel.orderOf_dvd_natCard_referenceSubgroup {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) {E : Type u_1} [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) f).Splits] {σ : Equiv.Perm ↑(f.rootSet E)} (hσ : σ ∈ (Polynomial.Gal.galActionHom f E).range) : orderOf σ ∣ Nat.card ↥(referenceSubgroup n j)

The order of a permutation of the roots induced by the Galois group of a polynomial with a label divides the order of the reference subgroup. The roots may be taken in any field where the polynomial splits.

theorem TauCeti.HasGaloisLabel.irreducible {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : Irreducible f

A polynomial with a label is irreducible, because every reference subgroup is transitive. There are no labels in degree zero, so no degree hypothesis is needed.

theorem TauCeti.HasGaloisLabel.eq_one_of_smul_eq_self {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) (hreg : Nat.card ↥(referenceSubgroup n j) = n) {E : Type u_1} [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) f).Splits] {σ : f.Gal} {x : ↑(f.rootSet E)} (hx : σ • x = x) : σ = 1

A regular label acts freely on the roots. If the reference subgroup of the label of f has as many elements as f has roots, then the only element of the Galois group of f fixing a root in a splitting extension E is the identity: the Galois group acts transitively on the roots and has as many elements as there are roots. Among the quartic labels this singles out the cyclic label 4T1, whose reference subgroup has order four, from the dihedral label 4T3.

theorem TauCeti.exists_hasGaloisLabel_of_irreducible {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = n) (h : ∀ (G : Subgroup (Equiv.Perm (Fin n))), MulAction.IsPretransitive (↥G) (Fin n) → ∃ (j : TransitiveGroupIndex n), TransitiveGroupLabel j G) : ∃ (j : TransitiveGroupIndex n), HasGaloisLabel f j

A label exists as soon as the classification supplies one. A separable irreducible polynomial of degree n carries a label in degree n provided every transitive subgroup of Equiv.Perm (Fin n) carries one, which the classification theorems of the low degrees prove.

theorem TauCeti.HasGaloisLabel.eq_of {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j k : TransitiveGroupIndex n} (h : ∀ {i i' : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))}, TransitiveGroupLabel i G → TransitiveGroupLabel i' G → i = i') (hj : HasGaloisLabel f j) (hk : HasGaloisLabel f k) : j = k

At most one label, as soon as the classification says so. A polynomial carries at most one label in degree n provided a subgroup of Equiv.Perm (Fin n) does, which the classification theorems of the low degrees prove. Transporting uniqueness from subgroups to polynomials does not see the degree.

theorem TauCeti.existsUnique_hasGaloisLabel {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = n) (hex : ∀ (G : Subgroup (Equiv.Perm (Fin n))), MulAction.IsPretransitive (↥G) (Fin n) → ∃ (i : TransitiveGroupIndex n), TransitiveGroupLabel i G) (huniq : ∀ {i i' : TransitiveGroupIndex n} {G : Subgroup (Equiv.Perm (Fin n))}, TransitiveGroupLabel i G → TransitiveGroupLabel i' G → i = i') : ∃! i : TransitiveGroupIndex n, HasGaloisLabel f i

Exactly one label, as soon as the classification supplies one and says it is unique. A separable irreducible polynomial of degree n carries exactly one label in degree n provided every transitive subgroup of Equiv.Perm (Fin n) carries exactly one.

theorem TauCeti.hasGaloisLabel_iff_natCard_gal {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (hsep : f.Separable) (hirr : Irreducible f) (hdeg : f.natDegree = n) (h : ∀ (G : Subgroup (Equiv.Perm (Fin n))), MulAction.IsPretransitive (↥G) (Fin n) → (TransitiveGroupLabel j G ↔ Nat.card ↥G = Nat.card ↥(referenceSubgroup n j))) : HasGaloisLabel f j ↔ Nat.card f.Gal = Nat.card ↥(referenceSubgroup n j)

A label is recognized by its order, as soon as the classification says so. A separable irreducible polynomial of degree n carries the label j exactly when its Galois group has the order of the reference subgroup, provided a transitive subgroup of Equiv.Perm (Fin n) carries the label j exactly when it has that order.

theorem TauCeti.HasGaloisLabel.isPreprimitive_iff {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : MulAction.IsPreprimitive ↥(Polynomial.Gal.galActionHom f f.SplittingField).range ↑(f.rootSet f.SplittingField) ↔ MulAction.IsPreprimitive (↥(referenceSubgroup n j)) (Fin n)

The Galois image of a polynomial with a label acts primitively on the roots exactly when the reference subgroup acts primitively.

theorem TauCeti.HasGaloisLabel.isSolvable_iff {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : Group.IsSolvable f.Gal ↔ Group.IsSolvable ↥(referenceSubgroup n j)

The Galois group of a polynomial with a label is solvable exactly when the reference subgroup is.

theorem TauCeti.HasGaloisLabel.isSolvable_iff_ne_five_or_lt_three {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : Group.IsSolvable f.Gal ↔ n ≠ 5 ∨ ↑j < 3

The solvability of a Galois group with a label. The Galois group of a polynomial with a label is solvable unless the label is 5T4 or 5T5. This is a statement about the group, not about solvableByRad.

theorem TauCeti.HasGaloisLabel.range_le_alternatingGroup_iff {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : (Polynomial.Gal.galActionHom f f.SplittingField).range ≤ alternatingGroup ↑(f.rootSet f.SplittingField) ↔ referenceSubgroup n j ≤ alternatingGroup (Fin n)

The Galois image of a polynomial with a label consists of even permutations of the roots exactly when the reference subgroup consists of even permutations.

theorem TauCeti.HasGaloisLabel.isSquare_discr_iff {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) (hf : f.Monic) (hchar : ringChar F ≠ 2) : IsSquare f.discr ↔ referenceSubgroup n j ≤ alternatingGroup (Fin n)

The discriminant reads the parity of the label. Away from characteristic 2, a monic polynomial with a label has a square discriminant exactly when the reference subgroup lies in the alternating group.

theorem TauCeti.HasGaloisLabel.range_le_alternatingGroup_iff_label {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : (Polynomial.Gal.galActionHom f f.SplittingField).range ≤ alternatingGroup ↑(f.rootSet f.SplittingField) ↔ n = 1 ∨ n = 3 ∧ ↑j = 0 ∨ n = 4 ∧ (↑j = 1 ∨ ↑j = 3) ∨ n = 5 ∧ (↑j = 0 ∨ ↑j = 1 ∨ ↑j = 3)

The Galois image of a labelled polynomial consists of even permutations exactly for the labels 1T1, 3T1, 4T2, 4T4, 5T1, 5T2, and 5T4.

theorem TauCeti.HasGaloisLabel.isSquare_discr_iff_label {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) (hf : f.Monic) (hchar : ringChar F ≠ 2) : IsSquare f.discr ↔ n = 1 ∨ n = 3 ∧ ↑j = 0 ∨ n = 4 ∧ (↑j = 1 ∨ ↑j = 3) ∨ n = 5 ∧ (↑j = 0 ∨ ↑j = 1 ∨ ↑j = 3)

Away from characteristic two, a monic labelled polynomial has square discriminant exactly for the labels 1T1, 3T1, 4T2, 4T4, 5T1, 5T2, and 5T4.

theorem TauCeti.HasGaloisLabel.irreducible_map_discrField_iff {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) (hf : f.Monic) (hchar : ringChar F ≠ 2) {E : Type u_1} [Field E] [Algebra F E] {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) : Irreducible (Polynomial.map (algebraMap F ↥(discrField f E)) f) ↔ MulAction.IsPretransitive (↥(referenceSubgroup n j ⊓ alternatingGroup (Fin n))) (Fin n)

Irreducibility over the discriminant field reads the even part of the label. Away from characteristic 2, a monic polynomial with a label stays irreducible over its discriminant field exactly when the even permutations in the reference subgroup act transitively. The discriminant field may be taken in any extension E containing a square root δ of the discriminant.

@[simp]

theorem TauCeti.hasGaloisLabel_one_iff {F : Type u} [Field F] {f : Polynomial F} (j : TransitiveGroupIndex 1) : HasGaloisLabel f j ↔ f.natDegree = 1

In degree one, a polynomial carries the label 1T1 exactly when it has degree one; such a polynomial is automatically separable.

@[simp]

theorem TauCeti.hasGaloisLabel_two_iff {F : Type u} [Field F] {f : Polynomial F} (j : TransitiveGroupIndex 2) : HasGaloisLabel f j ↔ f.Separable ∧ Irreducible f ∧ f.natDegree = 2

In degree two, a polynomial carries the label 2T1 exactly when it is separable, irreducible, and of degree two.

theorem TauCeti.HasGaloisLabel.isPreprimitive_gal_iff {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : MulAction.IsPreprimitive f.Gal ↑(f.rootSet f.SplittingField) ↔ MulAction.IsPreprimitive (↥(referenceSubgroup n j)) (Fin n)

The Galois group of a polynomial with a label acts primitively on its roots in the splitting field exactly when the reference subgroup acts primitively.

theorem TauCeti.HasGaloisLabel.isPreprimitive_gal_iff_ne_four_or_three_le {F : Type u} [Field F] {f : Polynomial F} {n : ℕ} {j : TransitiveGroupIndex n} (h : HasGaloisLabel f j) : MulAction.IsPreprimitive f.Gal ↑(f.rootSet f.SplittingField) ↔ n ≠ 4 ∨ 3 ≤ ↑j

The primitivity of a Galois group with a label. The Galois group of a polynomial with a label acts primitively on the roots in the splitting field exactly when the label is not one of 4T1, 4T2 and 4T3.