A finite family of universal integer Noether forms, with the exact degree and coefficient bound of CCDN Theorem 3.2.2.

Characteristic-zero nonvanishing of the ambient integer coefficient forms, descended from the algebraic closure.

Every absolutely irreducible characteristic-zero hypersurface of degree d at least two gives a nonzero Euler minor of order d²−1 in the universal affine-plane parameter ring.

theorem CCDN.exists_ambientNoetherForm_nonzero {K : Type u_1} {σ : Type u_2} [Field K] [CharZero K] [Fintype σ] [DecidableEq σ] (k : ℕ) (f : MvPolynomial (Option σ) K) (hf : f.IsHomogeneous (k + 2)) (hir : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : ∃ (rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ) (cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k) (m : PlaneParameters (Option σ) →₀ ℕ), (homogeneousCoefficientSpecialization (k + 2) f) (ambientNoetherForm (Option σ) k rows cols m) ≠ 0

Some constructed universal form detects every absolutely irreducible homogeneous equation in characteristic zero.

theorem CCDN.finite_ambientNoetherForms (σ : Type u_1) [Fintype σ] [DecidableEq σ] (k : ℕ) : {f : MvPolynomial (Sym σ (k + 2)) ℤ | ∃ (rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ) (cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k) (m : PlaneParameters σ →₀ ℕ), f = ambientNoetherForm σ k rows cols m}.Finite

For fixed σ and k, there are only finitely many ambient Noether forms.

noncomputable def CCDN.universalNoetherForms (σ : Type u_1) [Fintype σ] [DecidableEq σ] (k : ℕ) : Finset (MvPolynomial (Sym σ (k + 2)) ℤ)

The finite collection of universal Noether forms of degree k + 2 in the variables σ: the extracted plane-parameter coefficients of all Euler minors of the universal plane restriction of the universal homogeneous form.

Equations

• CCDN.universalNoetherForms σ k = ⋯.toFinset

theorem CCDN.universalNoetherForms_homogeneous {σ : Type u_1} [Fintype σ] [DecidableEq σ] (k : ℕ) (g : MvPolynomial (Sym σ (k + 2)) ℤ) (hg : g ∈ universalNoetherForms σ k) : g.IsHomogeneous ((k + 2) ^ 2 - 1)

Every universal Noether form is homogeneous of degree (k + 2) ^ 2 - 1.

theorem CCDN.universalNoetherForms_coefficientL1_le (n k : ℕ) (g : MvPolynomial (Sym (Option (Fin n)) (k + 2)) ℤ) (hg : g ∈ universalNoetherForms (Option (Fin n)) k) : g.l1Norm ≤ (k + 2) ^ (3 * (k + 2) ^ 2 - 3) * ((n + (k + 2)).choose n * 3 ^ (k + 2)) ^ ((k + 2) ^ 2 - 1)

The printed integer coefficient bound: in n + 1 homogeneous variables, every universal Noether form has coefficient ℓ¹-norm at most (k + 2) ^ (3 * (k + 2) ^ 2 - 3) * (choose (n + k + 2) n * 3 ^ (k + 2)) ^ ((k + 2) ^ 2 - 1).

theorem CCDN.universalNoetherForms_vanish {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [DecidableEq σ] (k : ℕ) (f : MvPolynomial σ K) (hf : f.IsHomogeneous (k + 2)) (hred : ¬Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (g : MvPolynomial (Sym σ (k + 2)) ℤ) (hg : g ∈ universalNoetherForms σ k) : (homogeneousCoefficientSpecialization (k + 2) f) g = 0

Every universal Noether form vanishes on a geometrically reducible homogeneous equation of degree k + 2, over an arbitrary field, with no characteristic assumption.

theorem CCDN.universalNoetherForms_nonvanishing {K : Type u_1} {σ : Type u_2} [Field K] [CharZero K] [Fintype σ] [DecidableEq σ] (k : ℕ) (f : MvPolynomial (Option σ) K) (hf : f.IsHomogeneous (k + 2)) (hir : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : ∃ g ∈ universalNoetherForms (Option σ) k, (homogeneousCoefficientSpecialization (k + 2) f) g ≠ 0

In characteristic zero, an absolutely irreducible homogeneous equation of degree k + 2 makes at least one universal Noether form nonzero.