The square root of the discriminant, and the test for the alternating group

Let f be a monic separable polynomial over a field F, and let E be an extension in which f splits. Numbering the roots of f in E by an equivalence e : Fin f.natDegree ≃ f.rootSet E turns the product of the root differences

δ = ∏_{i < j} (rᵢ - rⱼ)

into an element of E. Its square is the image of Polynomial.discr f, so δ is a square root of the discriminant; it is only a square root, because a different numbering changes δ by the sign of the permutation relating the two numberings.

That sign is the whole point. In a Galois splitting extension, a field automorphism of E over F permutes the roots, hence multiplies δ by the sign of the permutation it induces. When ringChar F ≠ 2, consequently δ lies in F exactly when the Galois image consists of even permutations, and — since δ² = discr f — that happens exactly when discr f is a square in F. This is the discriminant test for containment in the alternating group.

The characteristic hypothesis ringChar F ≠ 2 is not decoration. In characteristic 2 one has -1 = 1, so the sign never moves δ; inseparable monic polynomials have zero discriminant. Thus the discriminant of every monic polynomial is always a square, and the test decides nothing; this is recorded as Polynomial.Monic.isSquare_discr_of_char_two.

Main definitions

• TauCeti.discrSqrt: the product of the differences of the roots of f in E, taken over the pairs i < j of a numbering of the root set.

Main results

• Polynomial.Monic.discrSqrt_sq: discrSqrt e ^ 2 is the image of Polynomial.discr f in E.
• TauCeti.discrSqrt_trans: renumbering the roots by π multiplies discrSqrt by sign π.
• AlgEquiv.map_discrSqrt: an automorphism of E over F multiplies discrSqrt e by the sign of the permutation of the roots that it induces.
• Polynomial.Monic.isSquare_discr_iff_mem_range: discr f is a square in F exactly when discrSqrt e comes from F.
• TauCeti.discrSqrt_mem_range_iff: the root-difference product comes from F exactly when the Galois image is even; this does not require monicity.
• Polynomial.Monic.isSquare_discr_iff_range_le_alternatingGroup: the discriminant test, valid away from characteristic 2.
• Polynomial.Monic.isSquare_discr_of_char_two: in characteristic 2 the discriminant of every monic polynomial is a square, so the test is vacuous there.

References

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

The discriminant test

@[simp]

theorem AlgEquiv.map_discrSqrt {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)) (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : ϕ (TauCeti.discrSqrt e) = Equiv.Perm.sign ((Polynomial.Gal.galActionHom f E) ((Polynomial.Gal.restrict f E) ϕ)) • TauCeti.discrSqrt e

The transformation law for the square root of the discriminant. An automorphism ϕ of a splitting extension E over F multiplies the product of the root differences by the sign of the permutation that ϕ induces on the roots of f.

theorem TauCeti.discrSqrt_mem_range_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] (hchar : ringChar F ≠ 2) (e : Fin f.natDegree ≃ ↑(f.rootSet E)) : discrSqrt e ∈ Set.range ⇑(algebraMap F E) ↔ (Polynomial.Gal.galActionHom f E).range ≤ alternatingGroup ↑(f.rootSet E)

Away from characteristic 2, the product of the root differences comes from the base field exactly when the Galois image consists of even permutations of the roots.

theorem Polynomial.Monic.isSquare_discr_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) : IsSquare f.discr ↔ (Gal.galActionHom f E).range ≤ alternatingGroup ↑(f.rootSet E)

The discriminant test. For a monic separable polynomial over a field of characteristic other than 2, the discriminant is a square in the base field exactly when the Galois group acts on the roots by even permutations.

The characteristic hypothesis cannot be dropped: see Polynomial.Monic.isSquare_discr_of_char_two.

theorem Polynomial.Monic.isSquare_discr_of_char_two {F : Type u} [Field F] {f : Polynomial F} (hf : f.Monic) (hchar : ringChar F = 2) : IsSquare f.discr

In characteristic 2 the discriminant of every monic polynomial is a square. For a separable polynomial, the sign of a permutation acts trivially because -1 = 1, so the product of the root differences is fixed by the whole Galois group and therefore lies in the base field. For an inseparable polynomial, the discriminant is zero.

This is why the discriminant test carries the hypothesis ringChar F ≠ 2. The invariant that replaces the discriminant in characteristic 2 is Berlekamp's.