An irreducible section retaining the full total degree forces the original equation to be irreducible. Degree additivity prevents either nonconstant ambient factor from disappearing under restriction.

theorem CCDN.irreducible_of_full_degree_map {K : Type u_1} {σ : Type u_2} {τ : Type u_3} [Field K] (ψ : MvPolynomial σ K →+* MvPolynomial τ K) (hψ : ∀ (g : MvPolynomial σ K), (ψ g).totalDegree ≤ g.totalDegree) (f : MvPolynomial σ K) (hir : Irreducible (ψ f)) (hdeg : (ψ f).totalDegree = f.totalDegree) : Irreducible f

A degree-nonincreasing polynomial ring homomorphism reflects irreducibility at every equation whose full degree is retained.

noncomputable def CCDN.planeSectionPolynomialHom {K : Type u_1} {σ : Type u_2} [CommRing K] (v : PlaneParameters σ → K) : MvPolynomial σ K →+* MvPolynomial (Fin 2) K

The ring homomorphism restricting a polynomial in the coordinates σ to the affine plane a + s • b + t • c whose base point and directions are given by the parameters v, as a polynomial in the plane coordinates s and t.

Equations

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

theorem CCDN.irreducible_of_full_degree_planeSection {K : Type u_1} {σ : Type u_2} [Field K] (f : MvPolynomial σ K) (v : PlaneParameters σ → K) (hir : Irreducible (universalPlaneSection f v)) (hdeg : bivariateTotalDegree (universalPlaneSection f v) = f.totalDegree) : Irreducible f

If the plane section of f at parameters v is irreducible and keeps the total degree of f, then f is irreducible; the parameters v may be degenerate.