A primitive quartic for a biquadratic extension

If f, g, and f * g are nonsquares in a field of characteristic different from two, then sqrt f + sqrt g generates the corresponding biquadratic extension. Its minimal polynomial is

(X^2 - (f + g))^2 - 4 * f * g.

This file packages that calculation as a reusable irreducibility theorem.

noncomputable def BGS.Markoff.biquadraticPrimitiveQuartic {F : Type u_1} [Field F] (f g : F) : Polynomial F

The minimal-polynomial candidate for sqrt f + sqrt g.

Equations

• BGS.Markoff.biquadraticPrimitiveQuartic f g = (Polynomial.X ^ 2 - Polynomial.C (f + g)) ^ 2 - Polynomial.C (4 * f * g)

theorem BGS.Markoff.biquadraticPrimitiveQuartic_monic {F : Type u_1} [Field F] (f g : F) : (biquadraticPrimitiveQuartic f g).Monic

theorem BGS.Markoff.biquadraticPrimitiveQuartic_degree {F : Type u_1} [Field F] (f g : F) : (biquadraticPrimitiveQuartic f g).degree = 4

theorem BGS.Markoff.biquadraticPrimitiveQuartic_irreducible {F : Type u_1} [Field F] (h2 : 2 ≠ 0) {f g : F} (hf : ¬IsSquare f) (hg : ¬IsSquare g) (hfg : ¬IsSquare (f * g)) : Irreducible (biquadraticPrimitiveQuartic f g)

Three independent square classes give the irreducible primitive quartic of the associated biquadratic extension.