Universal Noether coefficient forms in an arbitrary ambient variable space. They are the plane-parameter coefficients of Euler minors.

noncomputable def CCDN.ambientEulerEntryLinear (R : Type u_1) (σ : Type u_2) [CommRing R] (k : ℕ) (row : ℕ × ℕ) (col : EulerColumns k) : MvPolynomial σ R →ₗ[R] MvPolynomial (PlaneParameters σ) R

The (row, col) entry of the Euler closed-form coefficient matrix of the universal plane restriction of a polynomial in the variables σ, as an R-linear function of that polynomial.

Equations

• CCDN.ambientEulerEntryLinear R σ k row col = ↑R (CCDN.eulerCoefficientEntryLinear k row col) ∘ₗ CCDN.universalPlanePolynomialLinear R σ

theorem CCDN.ambientEulerEntryLinear_apply {R : Type u_1} {σ : Type u_2} [CommRing R] (k : ℕ) (row : ℕ × ℕ) (col : EulerColumns k) (f : MvPolynomial σ R) : (ambientEulerEntryLinear R σ k row col) f = eulerClosedFormCoefficientMatrix k (universalPlanePolynomial f) row col

ambientEulerEntryLinear R σ k row col f is the (row, col) entry of the Euler closed-form coefficient matrix of the universal plane restriction of f.

theorem CCDN.ambientEulerEntryLinear_map {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommRing R] [CommRing S] (φ : R →+* S) (k : ℕ) (row : ℕ × ℕ) (col : EulerColumns k) (f : MvPolynomial σ R) : (ambientEulerEntryLinear S σ k row col) ((MvPolynomial.map φ) f) = (MvPolynomial.map φ) ((ambientEulerEntryLinear R σ k row col) f)

The entries ambientEulerEntryLinear commute with applying a coefficient ring homomorphism φ to the polynomial.

noncomputable def CCDN.ambientNoetherParameterMinor (σ : Type u_1) [Fintype σ] [DecidableEq σ] (k : ℕ) (rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ) (cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k) : MvPolynomial (PlaneParameters σ) (MvPolynomial (Sym σ (k + 2)) ℤ)

The minor with rows rows and columns cols of the Euler closed-form coefficient matrix of the universal plane restriction of the universal homogeneous form of degree k + 2. It is a polynomial in the plane parameters with coefficients that are integer polynomials in the coefficients of the form.

Equations

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

noncomputable def CCDN.ambientNoetherForm (σ : Type u_1) [Fintype σ] [DecidableEq σ] (k : ℕ) (rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ) (cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k) (m : PlaneParameters σ →₀ ℕ) : MvPolynomial (Sym σ (k + 2)) ℤ

The ambient Noether form indexed by a minor (rows, cols) and a plane-parameter monomial m: the coefficient of m in ambientNoetherParameterMinor σ k rows cols, an integer polynomial in the coefficients of a homogeneous form of degree k + 2.

Equations

• CCDN.ambientNoetherForm σ k rows cols m = (CCDN.ambientNoetherParameterMinor σ k rows cols).coeff m

theorem CCDN.ambientNoetherForm_homogeneous (σ : Type u_1) [Fintype σ] [DecidableEq σ] (k : ℕ) (rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ) (cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k) (m : PlaneParameters σ →₀ ℕ) : (ambientNoetherForm σ k rows cols m).IsHomogeneous ((k + 2) ^ 2 - 1)

Every extracted parameter coefficient is homogeneous of the exact Noether degree d²−1 in the original equation's coefficients.

theorem CCDN.ambientNoetherForm_specialize {R : Type u_1} {σ : Type u_2} [CommRing R] [Fintype σ] [DecidableEq σ] (k : ℕ) (f : MvPolynomial σ R) (hf : f.IsHomogeneous (k + 2)) (rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ) (cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k) (m : PlaneParameters σ →₀ ℕ) : (homogeneousCoefficientSpecialization (k + 2) f) (ambientNoetherForm σ k rows cols m) = ((eulerClosedFormCoefficientMatrix k (universalPlanePolynomial f)).submatrix rows cols).det.coeff m

Evaluation of a Noether form is exactly the corresponding coefficient of the restricted-equation determinant.