A nonzero universal minor of cubic parameter degree, over the original coefficient field; the nonvanishing proof descends from an algebraic closure. The leading coefficient of a universal plane section, evaluated by the highest homogeneous form in the first direction, detects loss of the full outer degree.

theorem CCDN.universalPlanePolynomial_map {K : Type u_1} {L : Type u_2} {σ : Type u_3} [CommRing K] [CommRing L] (φ : K →+* L) (f : MvPolynomial σ K) : universalPlanePolynomial ((MvPolynomial.map φ) f) = (bivariateMap (MvPolynomial.map φ)) (universalPlanePolynomial f)

The universal plane restriction commutes with applying a coefficient ring homomorphism.

theorem CCDN.exists_universalPlane_minor_degree {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (f : MvPolynomial (Option σ) K) (hf : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpos : 0 < f.totalDegree) (hchar : CharZeroOrGT K (2 * f.totalDegree ^ 2)) : ∃ (rows : Fin (2 * f.totalDegree ^ 2 - 1) → ℕ × ℕ) (cols : Fin (2 * f.totalDegree ^ 2 - 1) → ClosedFormColumns f.totalDegree), ((closedFormCoefficientMatrix f.totalDegree (universalPlanePolynomial f)).submatrix rows cols).det ≠ 0 ∧ ((closedFormCoefficientMatrix f.totalDegree (universalPlanePolynomial f)).submatrix rows cols).det.totalDegree ≤ (2 * f.totalDegree ^ 2 - 1) * f.totalDegree

A geometrically irreducible equation yields a nonzero polynomial in the full affine-plane parameter ring, of degree at most (2*d^2-1)*d. There are no smoothness or positioning hypotheses on the input equation.

noncomputable def CCDN.universalPlaneLeading {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) : MvPolynomial (PlaneParameters σ) K

The coefficient of x^d y^0, as a polynomial in all plane parameters.

Equations

• CCDN.universalPlaneLeading f = ((CCDN.universalPlanePolynomial f).coeff f.totalDegree).coeff 0

theorem CCDN.universalPlaneLeading_ne_zero_of_irreducible {K : Type u_1} {σ : Type u_2} [Field K] [IsAlgClosed K] [Finite σ] (f : MvPolynomial (Option σ) K) (hf : Irreducible f) (hpos : 0 < f.totalDegree) (hchar : CharZeroOrGT K f.totalDegree) : universalPlaneLeading f ≠ 0

Over an algebraically closed field, irreducibility and the characteristic bound suffice for the leading polynomial to be nonzero.

theorem CCDN.universalPlaneLeading_ne_zero {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (f : MvPolynomial (Option σ) K) (hf : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpos : 0 < f.totalDegree) (hchar : CharZeroOrGT K f.totalDegree) : universalPlaneLeading f ≠ 0

Geometric irreducibility and the characteristic bound suffice for the leading polynomial to be nonzero.