The discriminant field F(√disc f)

Let f be a polynomial over a field F and let E be an extension of F. The discriminant field of f in E is the subfield of E generated over F by the square roots of Polynomial.discr f that lie in E. It is TauCeti.discrField f E, defined as the adjunction to F of the root set of X ^ 2 - C f.discr in E.

Whenever E contains an element δ with δ ^ 2 = discr f — for monic separable f splitting in E the square root TauCeti.discrSqrt of the previous file is one — the definition collapses to the simple extension F⟮δ⟯, because the only other square root of the discriminant is -δ, and it is then a splitting field of X ^ 2 - C f.discr over F. (When E contains no square root at all the root set is empty and the discriminant field is just F.) In particular the discriminant field does not depend on the numbering of the roots that discrSqrt is computed from, even though discrSqrt itself changes sign with it. From that description one reads off the two possibilities: F⟮δ⟯ is F when discr f is a square in F, and a quadratic extension of F otherwise. Away from characteristic 2 it is moreover a Galois extension of F as soon as the discriminant is nonzero, since X ^ 2 - C f.discr is then separable.

The discriminant field is determined by the discriminant alone. The comparison theorem TauCeti.fixedField_evenAutSubgroup characterizes it additionally through the action on the roots of f: in a Galois splitting extension and away from characteristic 2, the discriminant field is exactly the field fixed by the automorphisms that permute the roots of f evenly. That subgroup is TauCeti.evenAutSubgroup f E. The transformation law AlgEquiv.map_discrSqrt makes both inclusions short: an even automorphism fixes δ, and an odd one negates it, which is a genuine move because δ ≠ 0 and 2 ≠ 0.

The same comparison reads factorizations over the discriminant field on the Galois image: in a normal splitting extension, f stays irreducible over its discriminant field exactly when the even permutations in the Galois image act transitively on the roots (TauCeti.irreducible_map_discrField_iff). Since all discriminant fields are splitting fields of X ^ 2 - C f.discr, whether f stays irreducible over one does not depend on the extension E in which it is taken (TauCeti.irreducible_map_discrField_congr). This is the datum that separates the cyclic quartic group from the dihedral one, whose even parts are respectively intransitive and transitive. The discriminant test of the previous file is recovered here as the statement that the discriminant field is trivial exactly when the Galois image is contained in the alternating group.

Main definitions

• TauCeti.discrField: the subfield of E generated over F by the square roots of discr f.
• TauCeti.evenAutSubgroup: the automorphisms of a splitting extension E over F that induce an even permutation of the roots of f.

Main results

• TauCeti.discrField_eq_adjoin_simple: a square root δ of the discriminant generates the discriminant field.
• TauCeti.isSplittingField_discrField: if E contains a square root of the discriminant, the discriminant field is a splitting field of X ^ 2 - C f.discr.
• TauCeti.discrField_map: it is natural in the extension.
• TauCeti.discrField_baseChange: after extending the base field, it is the compositum of the new base field with the original discriminant field.
• TauCeti.discrField_eq_bot_iff, TauCeti.finrank_discrField_eq_two: the discriminant field is F exactly when the discriminant is a square, and has degree 2 otherwise.
• TauCeti.isGalois_discrField: away from characteristic 2, and for nonzero discriminant, it is a Galois extension of F.
• TauCeti.irreducible_map_discrField_congr: irreducibility over the discriminant field does not depend on the extension in which the discriminant field is taken.
• TauCeti.fixedField_evenAutSubgroup: the comparison theorem, that the discriminant field is the fixed field of the even part of the Galois group, and TauCeti.fixingSubgroup_discrField: conversely, the even part of the Galois group is the subgroup fixing the discriminant field.
• TauCeti.irreducible_map_discrField_iff: f stays irreducible over the discriminant field exactly when the even part of its Galois image is transitive on the roots.
• TauCeti.discrField_eq_bot_iff_range_le_alternatingGroup, TauCeti.finrank_discrField_eq_two_iff: the discriminant test, read on the discriminant field.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, §6.3.

The discriminant field

def TauCeti.discrField {F : Type u} [Field F] (f : Polynomial F) (E : Type v) [Field E] [Algebra F E] : IntermediateField F E

The discriminant field of f in E: the subfield of E generated over F by the square roots of Polynomial.discr f that lie in E. If E contains such a square root this is a splitting field of X ^ 2 - C f.discr over F (TauCeti.isSplittingField_discrField); if it contains none, the root set is empty and the discriminant field is F itself.

TauCeti.discrField_eq_adjoin_simple describes it as F⟮δ⟯ for any square root δ of the discriminant in E. Stating it as an adjunction of the whole root set instead of a simple extension keeps it independent of the choice of square root, hence of the numbering of the roots of f that TauCeti.discrSqrt is computed from.

Equations

• TauCeti.discrField f E = IntermediateField.adjoin F ((Polynomial.X ^ 2 - Polynomial.C f.discr).rootSet E)

theorem TauCeti.discrField_def {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} : discrField f E = IntermediateField.adjoin F ((Polynomial.X ^ 2 - Polynomial.C f.discr).rootSet E)

The discriminant field is generated by the roots of the discriminant quadratic.

theorem TauCeti.discrField_eq_adjoin_simple {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) : discrField f E = F⟮δ⟯

Any square root of the discriminant in E generates the discriminant field.

theorem TauCeti.isSplittingField_discrField {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) : Polynomial.IsSplittingField F (↥(discrField f E)) (Polynomial.X ^ 2 - Polynomial.C f.discr)

If E contains a square root of the discriminant, then the discriminant field is a splitting field of X ^ 2 - C f.discr over F; Polynomial.IsSplittingField.algEquiv therefore identifies it with the abstract splitting field of that polynomial.

@[simp]

theorem TauCeti.discrField_map {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {E' : Type w} [Field E'] [Algebra F E'] (ψ : E ≃ₐ[F] E') : IntermediateField.map (↑ψ) (discrField f E) = discrField f E'

Naturality in the extension. An F-isomorphism of extensions carries the discriminant field of f in one to the discriminant field of f in the other. Taking E' = E it says that every F-automorphism of E maps the discriminant field onto itself.

theorem TauCeti.discrField_baseChange {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {K : Type w} [Field K] [Algebra F K] [Algebra K E] [IsScalarTower F K E] : discrField (Polynomial.map (algebraMap F K) f) E = IntermediateField.adjoin K ↑(discrField f E)

Base change of the discriminant field. In a tower E / K / F, the discriminant field of f after extending scalars from F to K is the compositum in E of K with the original discriminant field. Since a field extension preserves polynomial degree, no hypothesis on f is needed. When E contains a square root of f.discr and the image of f.discr remains a nonsquare in K, the base-changed field is still quadratic over K by TauCeti.finrank_discrField_baseChange_eq_two.

theorem TauCeti.discrField_eq_bot_iff {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) : discrField f E = ⊥ ↔ IsSquare f.discr

The trivial case. Once E contains a square root of the discriminant, the discriminant field is the base field exactly when the discriminant is a square in the base field.

theorem TauCeti.finrank_discrField_eq_one_iff {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) : Module.finrank F ↥(discrField f E) = 1 ↔ IsSquare f.discr

The discriminant field is trivial exactly when it has degree one over the base field.

theorem TauCeti.finrank_discrField_eq_two {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) (hsq : ¬IsSquare f.discr) : Module.finrank F ↥(discrField f E) = 2

The quadratic case. When the discriminant is not a square in the base field, the discriminant field is a quadratic extension of it.

theorem TauCeti.finrank_discrField_baseChange_eq_two {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {K : Type w} [Field K] [Algebra F K] [Algebra K E] [IsScalarTower F K E] {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) (hsq : ¬IsSquare ((algebraMap F K) f.discr)) : Module.finrank K ↥(IntermediateField.adjoin K ↑(discrField f E)) = 2

If E contains a square root of the discriminant and the discriminant remains a nonsquare after extending scalars from F to K, then the compositum of K with the original discriminant field is quadratic over K. This is the quadratic, nonsplit case of TauCeti.discrField_baseChange.

theorem TauCeti.isGalois_discrField {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {δ : E} (hδ : δ ^ 2 = (algebraMap F E) f.discr) (hdisc : f.discr ≠ 0) (hchar : ringChar F ≠ 2) : IsGalois F ↥(discrField f E)

Away from characteristic 2, the discriminant field of a polynomial with nonzero discriminant is a Galois extension of the base field: it is the splitting field of X ^ 2 - C f.discr, which is separable because the discriminant is nonzero and 2 is invertible. For a monic polynomial, Polynomial.Monic.discr_ne_zero_iff reads the hypothesis as separability of f.

theorem TauCeti.irreducible_map_discrField_congr {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} {E' : Type w} [Field E'] [Algebra F E'] {δ : E} {δ' : E'} (hδ : δ ^ 2 = (algebraMap F E) f.discr) (hδ' : δ' ^ 2 = (algebraMap F E') f.discr) (g : Polynomial F) : Irreducible (Polynomial.map (algebraMap F ↥(discrField f E)) g) ↔ Irreducible (Polynomial.map (algebraMap F ↥(discrField f E')) g)

Irreducibility over the discriminant field does not depend on the ambient extension. If E and E' both contain a square root of the discriminant of f, then a polynomial g is irreducible over the discriminant field of f in E exactly when it is irreducible over the discriminant field of f in E': both are splitting fields of X ^ 2 - C f.discr, hence isomorphic over F.

The comparison with the even part of the Galois group

noncomputable def TauCeti.evenAutSubgroup {F : Type u} [Field F] (f : Polynomial F) (E : Type v) [Field E] [Algebra F E] [Fact (Polynomial.map (algebraMap F E) f).Splits] : Subgroup Gal(E/F)

The even part of the Galois group. For a splitting extension E of f over F, this is the subgroup of automorphisms of E over F that permute the roots of f evenly. It is the kernel of the sign of the root action, hence a normal subgroup of index at most two.

Equations

• TauCeti.evenAutSubgroup f E = Subgroup.comap (Polynomial.Gal.restrict f E) (Subgroup.comap (Polynomial.Gal.galActionHom f E) (alternatingGroup ↑(f.rootSet E)))

@[simp]

theorem TauCeti.mem_evenAutSubgroup {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] {ϕ : Gal(E/F)} : ϕ ∈ evenAutSubgroup f E ↔ Equiv.Perm.sign ((Polynomial.Gal.galActionHom f E) ((Polynomial.Gal.restrict f E) ϕ)) = 1

theorem TauCeti.evenAutSubgroup_eq_fixingSubgroup {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] (hchar : ringChar F ≠ 2) (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : evenAutSubgroup f E = F⟮discrSqrt e⟯.fixingSubgroup

The even part of the Galois group is the subgroup fixing the root-difference product. Both inclusions are the transformation law AlgEquiv.map_discrSqrt: an even automorphism fixes the product, and an odd one negates it, which moves it because it is nonzero and 2 ≠ 0.

theorem TauCeti.fixingSubgroup_discrField {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] (hf : f.Monic) (hsep : f.Separable) (hchar : ringChar F ≠ 2) : (discrField f E).fixingSubgroup = evenAutSubgroup f E

The comparison theorem, from the other side. Away from characteristic 2, the automorphisms of a splitting extension that fix the discriminant field of a monic separable polynomial are exactly those acting on its roots by an even permutation. Unlike TauCeti.fixedField_evenAutSubgroup, this needs no normality of the extension.

theorem TauCeti.fixedField_evenAutSubgroup {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] [IsGalois F E] (hf : f.Monic) (hsep : f.Separable) (hchar : ringChar F ≠ 2) : IntermediateField.fixedField (evenAutSubgroup f E) = discrField f E

The comparison theorem. In a Galois splitting extension, and away from characteristic 2, the discriminant field of a monic separable polynomial is the field fixed by the automorphisms acting on the roots by an even permutation.

theorem TauCeti.isPretransitive_evenAutSubgroup_iff {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] [Normal F E] : MulAction.IsPretransitive ↥(evenAutSubgroup f E) ↑(f.rootSet E) ↔ MulAction.IsPretransitive ↥((Polynomial.Gal.galActionHom f E).range ⊓ alternatingGroup ↑(f.rootSet E)) ↑(f.rootSet E)

In a normal splitting extension, the even part of the automorphism group acts transitively on the roots exactly when the even permutations in the Galois image do. The root action maps the former onto the latter, because every element of f.Gal lifts to an automorphism of E.

theorem TauCeti.irreducible_map_discrField_iff {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] [Normal F E] (hf : f.Monic) (hsep : f.Separable) (hchar : ringChar F ≠ 2) (hdeg : 0 < f.natDegree) : Irreducible (Polynomial.map (algebraMap F ↥(discrField f E)) f) ↔ MulAction.IsPretransitive ↥((Polynomial.Gal.galActionHom f E).range ⊓ alternatingGroup ↑(f.rootSet E)) ↑(f.rootSet E)

Irreducibility over the discriminant field. In a normal splitting extension, and away from characteristic 2, a monic separable polynomial of positive degree stays irreducible over its discriminant field exactly when the even permutations in its Galois image act transitively on its roots.

By TauCeti.irreducible_map_discrField_congr, the left-hand side is the same for the discriminant field taken in any extension containing a square root of the discriminant.

theorem TauCeti.discrField_eq_bot_iff_range_le_alternatingGroup {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] [IsGalois F E] (hf : f.Monic) (hsep : f.Separable) (hchar : ringChar F ≠ 2) : discrField f E = ⊥ ↔ (Polynomial.Gal.galActionHom f E).range ≤ alternatingGroup ↑(f.rootSet E)

The discriminant test, read on the discriminant field. The discriminant field is trivial exactly when the Galois image consists of even permutations of the roots.

theorem TauCeti.finrank_discrField_eq_two_iff {F : Type u} [Field F] {E : Type v} [Field E] [Algebra F E] {f : Polynomial F} [Fact (Polynomial.map (algebraMap F E) f).Splits] [IsGalois F E] (hf : f.Monic) (hsep : f.Separable) (hchar : ringChar F ≠ 2) : Module.finrank F ↥(discrField f E) = 2 ↔ ¬(Polynomial.Gal.galActionHom f E).range ≤ alternatingGroup ↑(f.rootSet E)

The discriminant field is a quadratic extension exactly when the Galois image contains an odd permutation of the roots. This is the separation the quartic decision table reads.