Ordinary irreducibility of f(x,yz_1,...,yz_n) over the rational function field in the slopes z_i. The original equation is irreducible and monic in x; all parameter extensions and changes of polynomial presentation are proved.

noncomputable def CCDN.genericPlaneCoefficients (K : Type u_1) (σ : Type u_2) [Field K] : MvPolynomial σ K →ₐ[K] Polynomial (MvPolynomial σ K)

Replace each transverse variable z_i with the polynomial z_i*y.

Equations

• CCDN.genericPlaneCoefficients K σ = MvPolynomial.aeval fun (i : σ) => Polynomial.C (MvPolynomial.X i) * Polynomial.X

noncomputable def CCDN.genericPlanePolynomial {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial (Option σ) K) : Polynomial (Polynomial (MvPolynomial σ K))

The generic plane equation, with x outermost and y the inner variable.

Equations

• CCDN.genericPlanePolynomial f = Polynomial.map (CCDN.genericPlaneCoefficients K σ).toRingHom ((MvPolynomial.optionEquivLeft K σ) f)

theorem CCDN.genericPlanePolynomial_monic {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial (Option σ) K) (hf : ((MvPolynomial.optionEquivLeft K σ) f).Monic) : (genericPlanePolynomial f).Monic

If f is monic in its distinguished variable, then so is the generic plane equation of f.

theorem CCDN.genericPlanePolynomial_natDegree {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial (Option σ) K) (hf : ((MvPolynomial.optionEquivLeft K σ) f).Monic) : (genericPlanePolynomial f).natDegree = ((MvPolynomial.optionEquivLeft K σ) f).natDegree

If f is monic in its distinguished variable, then the generic plane equation of f has the same degree in that variable.

theorem CCDN.genericPlanePolynomial_irreducible_fraction_slopes {K : Type u_1} {F : Type u_2} {σ : Type u_3} [Field K] [Field F] [Algebra (MvPolynomial σ K) F] [IsFractionRing (MvPolynomial σ K) F] (f : MvPolynomial (Option σ) K) (hf : Irreducible f) (hd : 0 < f.totalDegree) (hm : ((MvPolynomial.optionEquivLeft K σ) f).Monic) (hx : 0 < ((MvPolynomial.optionEquivLeft K σ) f).natDegree) : Irreducible ((bivariateMap (algebraMap (MvPolynomial σ K) F)) (genericPlanePolynomial f))

Localizing the slope parameters preserves the ordinary irreducibility of the generic plane equation.