Base change of absolutely irreducible multivariate polynomials

An irreducible multivariate polynomial over an algebraic closure remains irreducible after extending its original coefficient field to an arbitrary field. The proof is a direct Nullstellensatz descent. Given a hypothetical factorization over the target field, introduce one variable for each of its finitely many coefficients and two additional variables for inverses of chosen nonconstant coefficients. A closed point of a maximal ideal over the kernel specializes the factorization to the algebraically closed field, while the inverse relations ensure that both specialized factors remain nonunits.

The final theorem supplies the exact constant-field base-change step used in Corvaja--Zannier's auxiliary-family argument.

theorem BGS.CorvajaZannier.irreducible_map_of_irreducible_map_isAlgClosed {K : Type u_1} {E : Type u_2} {F : Type u_3} {σ : Type u_4} [Field K] [Field E] [Field F] [Algebra K E] [IsAlgClosed E] (iF : K →+* F) (f : MvPolynomial σ K) (hE : Irreducible ((MvPolynomial.map (algebraMap K E)) f)) : Irreducible ((MvPolynomial.map iF) f)

If a multivariate polynomial is irreducible after extension to an algebraically closed field, it remains irreducible after any other injective field extension of its original coefficient field.

theorem BGS.CorvajaZannier.irreducible_map_of_irreducible_map_algebraicClosure {K : Type u_5} {F : Type u_6} {σ : Type u_7} [Field K] [Field F] (iF : K →+* F) (f : MvPolynomial σ K) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : Irreducible ((MvPolynomial.map iF) f)

Absolute irreducibility, stated using AlgebraicClosure K, implies irreducibility after an arbitrary field-valued coefficient embedding.

theorem BGS.CorvajaZannier.irreducible_map_perfectConstantsToFrobeniusSubfield {K : Type u_5} {L : Type u_6} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] (f : MvPolynomial (Fin 2) K) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : Irreducible ((MvPolynomial.map perfectConstantsToFrobeniusSubfield) f)

The exact base-change bridge needed by the plane-curve auxiliary-family theorem: absolute irreducibility over K implies irreducibility after extension of constants to the Frobenius subfield L^p.