Ordinary irreducibility of the generic stretching substitution f(x,z) -> f(x,y*z). The fresh variable y is first made invertible; scaling then becomes a polynomial automorphism. Monicity in x descends irreducibility back to the polynomial coefficient ring.

noncomputable def CCDN.variableScaleEquiv (K : Type u_1) (σ : Type u_2) [Field K] (a : K) (ha : a ≠ 0) : MvPolynomial σ K ≃ₐ[K] MvPolynomial σ K

Simultaneously multiply all polynomial variables by a nonzero scalar.

Equations

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

@[simp]

theorem CCDN.variableScaleEquiv_X {K : Type u_1} {σ : Type u_2} [Field K] (a : K) (ha : a ≠ 0) (i : σ) : (variableScaleEquiv K σ a ha) (MvPolynomial.X i) = MvPolynomial.C a * MvPolynomial.X i

The scaling automorphism by a sends each variable X i to a * X i.

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

Introduce a fresh polynomial parameter and scale each transverse variable by that parameter, keeping the distinguished outer variable fixed.

Equations

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

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

The generic stretch f(x, z) ↦ f(x, y * z) of f, viewed as a polynomial in the distinguished outer variable x whose coefficients involve the transverse variables z and the fresh parameter y.

Equations

• CCDN.genericPlaneStretch f = Polynomial.map (CCDN.genericStretchCoefficients K σ).toRingHom ((MvPolynomial.optionEquivLeft K σ) f)

theorem CCDN.genericPlaneStretch_irreducible {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial (Option σ) K) (hf : Irreducible f) (hd : 0 < f.totalDegree) (hm : ((MvPolynomial.optionEquivLeft K σ) f).Monic) : Irreducible (genericPlaneStretch f)

The generic stretch is ordinarily irreducible before any slope parameters are specialized or localized.