The constructed ambient coefficient forms vanish on every geometrically reducible homogeneous equation, in every characteristic.
theorem
CCDN.universalPlanePolynomial_totalDegree_le
{R : Type u_1}
{σ : Type u_2}
[CommRing R]
(f : MvPolynomial σ R)
:
The universal plane restriction of f has bivariate total degree at most the total degree of
f.
theorem
CCDN.ambientEuler_minor_eq_zero_of_product
{R : Type u_1}
{σ : Type u_2}
[CommRing R]
(k a b : ℕ)
(ha : 0 < a)
(hb : 0 < b)
(hab : a + b = k + 2)
(g h : MvPolynomial σ R)
(hg : g.totalDegree ≤ a)
(hh : h.totalDegree ≤ b)
(rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ)
(cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k)
:
((eulerClosedFormCoefficientMatrix k (universalPlanePolynomial (g * h))).submatrix rows cols).det = 0
If g and h have total degrees at most a and b, with a, b > 0 and a + b = k + 2,
then every minor of order (k + 2)^2 - 1 of the Euler closed-form coefficient matrix of the
universal plane restriction of g * h vanishes.
theorem
CCDN.ambientEuler_minor_map
{R : Type u_1}
{S : Type u_2}
{σ : Type u_3}
[CommRing R]
[CommRing S]
(φ : R →+* S)
(k : ℕ)
(f : MvPolynomial σ R)
(rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ)
(cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k)
:
(MvPolynomial.map φ) ((eulerClosedFormCoefficientMatrix k (universalPlanePolynomial f)).submatrix rows cols).det = ((eulerClosedFormCoefficientMatrix k (universalPlanePolynomial ((MvPolynomial.map φ) f))).submatrix rows cols).det
Minors of the Euler closed-form coefficient matrix of the universal plane restriction commute
with applying a coefficient ring homomorphism φ to the polynomial.
theorem
CCDN.ambientNoetherForm_eq_zero_of_not_absolutely_irreducible
{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))
(rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ)
(cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k)
(m : PlaneParameters σ →₀ ℕ)
:
The first implication in the universal Noether theorem, for the constructed integer coefficient forms and arbitrary characteristic.