Discriminants of quartics and their resolvent cubics

A monic quartic of degree four and the cubic obtained by specializing quarticD4Spec have the same discriminant. Consequently, the specialized resolvent is separable exactly when the quartic is separable, so downstream quartic Galois-group criteria require no additional separation hypothesis.

For the depressed quartic

X⁴ + pX² + qX + r

and its cubic resolvent

X³ - pX² - 4rX + (4pr - q²)

the specialized resolvent is TauCeti.resolventCubic p q r, giving the corresponding closed-form identity and separability results. All these statements hold over an arbitrary commutative ring.

Main results

• Polynomial.Monic.discr_of_natDegree_eq_four: the coefficient formula for the discriminant of a monic quartic.
• TauCeti.discr_depressedQuartic: the explicit discriminant of a depressed quartic.
• TauCeti.discr_quarticD4Spec_specialize: a monic quartic of degree four and its specialized resolvent have equal discriminants.
• TauCeti.separable_quarticD4Spec_specialize_iff: the quartic is separable exactly when its specialized resolvent is.
• TauCeti.discr_resolventCubic: a depressed quartic and its resolvent cubic have equal discriminants.
• TauCeti.separable_resolventCubic_iff: the quartic is separable exactly when its resolvent is.
• TauCeti.separable_resolventCubic: a separable quartic has a separable resolvent cubic.

References

• K. Conrad, Galois groups of cubics and quartics (not in characteristic 2), Theorem 3.4.

theorem TauCeti.discr_quarticD4Spec_specialize {R : Type u_1} [CommRing R] {f : Polynomial R} (hmonic : f.Monic) (hf : f.natDegree = 4) : f.discr = (quarticD4Spec.specialize R f).discr

A monic quartic of degree four and the specialization of the quartic D₄ resolvent have the same discriminant.

theorem TauCeti.separable_quarticD4Spec_specialize_iff {R : Type u_1} [CommRing R] {f : Polynomial R} (hmonic : f.Monic) (hf : f.natDegree = 4) : (quarticD4Spec.specialize R f).Separable ↔ f.Separable

The specialization of the quartic D₄ resolvent is separable exactly when the monic quartic of degree four is separable.

theorem TauCeti.discr_resolventCubic {R : Type u_1} [CommRing R] (p q r : R) : (Polynomial.X ^ 4 + Polynomial.C p * Polynomial.X ^ 2 + Polynomial.C q * Polynomial.X + Polynomial.C r).discr = (resolventCubic p q r).discr

A depressed quartic and its resolvent cubic have the same discriminant.

@[simp]

theorem TauCeti.separable_resolventCubic_iff {R : Type u_1} [CommRing R] (p q r : R) : (resolventCubic p q r).Separable ↔ (Polynomial.X ^ 4 + Polynomial.C p * Polynomial.X ^ 2 + Polynomial.C q * Polynomial.X + Polynomial.C r).Separable

The resolvent cubic of a depressed quartic is separable exactly when the quartic is separable. This holds over every commutative ring, where separability of a monic polynomial is equivalent to its discriminant being a unit.

theorem TauCeti.separable_resolventCubic {R : Type u_1} [CommRing R] (p q r : R) (h : (Polynomial.X ^ 4 + Polynomial.C p * Polynomial.X ^ 2 + Polynomial.C q * Polynomial.X + Polynomial.C r).Separable) : (resolventCubic p q r).Separable

The resolvent cubic of a separable depressed quartic is separable.