The generic plane f(x,y*z), with slopes in their rational function field, has a smooth origin whenever the original equation does. Together with ordinary irreducibility this proves geometric irreducibility of the generic plane in the positioned coordinates.

noncomputable def CCDN.genericPlaneMap (K : Type u_1) (F : Type u_2) (σ : Type u_3) [Field K] [Field F] [Algebra K F] [Algebra (MvPolynomial σ K) F] : MvPolynomial (Option σ) K →ₐ[K] MvPolynomial (Fin 2) F

The generic plane substitution as a map of multivariate polynomial rings.

Equations

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

theorem CCDN.genericPlaneMap_bivariate {K : Type u_1} {F : Type u_2} {σ : Type u_3} [Field K] [Field F] [Algebra K F] [Algebra (MvPolynomial σ K) F] [IsScalarTower K (MvPolynomial σ K) F] (f : MvPolynomial (Option σ) K) : (bivariatePolynomialEquiv F) ((genericPlaneMap K F σ) f) = (bivariateMap (algebraMap (MvPolynomial σ K) F)) (genericPlanePolynomial f)

The generic plane substitution genericPlaneMap K F σ f corresponds, as a bivariate polynomial over F, to the generic plane equation genericPlanePolynomial f with its coefficients mapped into F.

theorem CCDN.genericPlaneMap_eval_zero {K : Type u_1} {F : Type u_2} {σ : Type u_3} [Field K] [Field F] [Algebra K F] [Algebra (MvPolynomial σ K) F] (f : MvPolynomial (Option σ) K) : (MvPolynomial.eval 0) ((genericPlaneMap K F σ) f) = (algebraMap K F) ((MvPolynomial.eval 0) f)

The generic plane section of f takes at the origin the value f(0).

theorem CCDN.genericPlaneMap_pderiv {K : Type u_1} {F : Type u_2} {σ : Type u_3} [Field K] [Field F] [Algebra K F] [Algebra (MvPolynomial σ K) F] (f : MvPolynomial (Option σ) K) : (MvPolynomial.pderiv 0) ((genericPlaneMap K F σ) f) = (genericPlaneMap K F σ) ((MvPolynomial.pderiv none) f)

The derivative of the generic plane section of f in its first variable is the generic plane section of the derivative of f in the distinguished variable none.

theorem CCDN.genericPlaneMap_irreducible {K : Type u_1} {F : Type u_2} {σ : Type u_3} [Field K] [Field F] [Algebra K F] [Algebra (MvPolynomial σ K) F] [IsScalarTower K (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 ((genericPlaneMap K F σ) f)

Ordinary irreducibility over the rational function field in slopes.