Explicit absolutely irreducible equations through a Cartesian grid. The construction uses Eisenstein at the inner coordinate zero.

noncomputable def CCDN.gridEisensteinCorrection {K : Type u_1} [Field K] (V : Polynomial K) (k : ℕ) : Polynomial K

The inner correction has prescribed degree and makes the first coefficient of the constant outer coefficient nonzero.

Equations

• CCDN.gridEisensteinCorrection V k = V * (Polynomial.X ^ k + Polynomial.C (V.coeff 1 / V.coeff 0 + 1) * Polynomial.X)

noncomputable def CCDN.gridEisensteinPolynomial {K : Type u_1} [Field K] (V : Polynomial K) (k : ℕ) : Polynomial (Polynomial K)

The outer variable is the first coordinate, the inner variable the second. At roots of V in both coordinates all three summands vanish.

Equations

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

theorem CCDN.gridEisensteinPolynomial_coeff {K : Type u_1} [Field K] (V : Polynomial K) (k i : ℕ) : (gridEisensteinPolynomial V k).coeff i = Polynomial.C (V.coeff i) + V * Polynomial.C (V.coeff 0)⁻¹ * ((Polynomial.X ^ V.natDegree).coeff i - Polynomial.C (V.coeff i)) + if i = 0 then gridEisensteinCorrection V k else 0

The i-th coefficient of gridEisensteinPolynomial V k in the outer variable, written out from its three summands.

theorem CCDN.gridEisensteinPolynomial_irreducible {K : Type u_1} [Field K] (V : Polynomial K) (k : ℕ) (hm : V.Monic) (hd : 0 < V.natDegree) (h0 : V.coeff 0 ≠ 0) (hk : 2 ≤ k) : Irreducible (gridEisensteinPolynomial V k)

Absolute irreducibility of the explicit construction, over every field.

theorem CCDN.gridEisensteinPolynomial_eval_zero {K : Type u_1} [Field K] (V : Polynomial K) (k : ℕ) (x y : K) (hx : Polynomial.eval x V = 0) (hy : Polynomial.eval y V = 0) : Polynomial.eval x (Polynomial.map (Polynomial.evalRingHom y) (gridEisensteinPolynomial V k)) = 0

gridEisensteinPolynomial V k vanishes at every point (x, y) whose coordinates are both roots of V.