An explicit parameter space for Euler-constrained polynomial pairs. For degree d=k+2, its dimension is d^2-1: two polynomials of degree at most k and one homogeneous polynomial of degree k.

@[reducible, inline]

abbrev CCDN.EulerPairSpace (R : Type u_1) [CommRing R] (k : ℕ) : Type u_1

The parameter space of Euler-constrained pairs: triples (A, B, Q) with A and B bivariate polynomials of total degree at most k and Q homogeneous of degree k.

Equations

• CCDN.EulerPairSpace R k = (↥(MvPolynomial.restrictTotalDegree (Fin 2) R k) × ↥(MvPolynomial.restrictTotalDegree (Fin 2) R k) × ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R k))

noncomputable def CCDN.eulerPairCoordinates (R : Type u_1) [CommRing R] (k : ℕ) : EulerPairSpace R k →ₗ[R] MvPolynomial (Fin 2) R × MvPolynomial (Fin 2) R

(A,B,Q) gives (A+yQ,B-xQ), so the two top-degree radial terms cancel.

Equations

• CCDN.eulerPairCoordinates R k = { toFun := fun (u : CCDN.EulerPairSpace R k) => (↑u.1 + MvPolynomial.X 1 * ↑u.2.2, ↑u.2.1 - MvPolynomial.X 0 * ↑u.2.2), map_add' := ⋯, map_smul' := ⋯ }

theorem CCDN.eulerPairCoordinates_fst_degree {R : Type u_1} [CommRing R] (k : ℕ) (u : EulerPairSpace R k) : ((eulerPairCoordinates R k) u).1.totalDegree ≤ k + 1

The first polynomial A + y * Q of an Euler pair has total degree at most k + 1.

theorem CCDN.eulerPairCoordinates_snd_degree {R : Type u_1} [CommRing R] (k : ℕ) (u : EulerPairSpace R k) : ((eulerPairCoordinates R k) u).2.totalDegree ≤ k + 1

The second polynomial B - x * Q of an Euler pair has total degree at most k + 1.

theorem CCDN.eulerPairCoordinates_contraction_degree {R : Type u_1} [CommRing R] (k : ℕ) (u : EulerPairSpace R k) : (MvPolynomial.X 0 * ((eulerPairCoordinates R k) u).1 + MvPolynomial.X 1 * ((eulerPairCoordinates R k) u).2).totalDegree ≤ k + 1

The radial contraction x * P + y * Q of the pair (P, Q) attached to an element of EulerPairSpace R k has total degree at most k + 1.

theorem CCDN.eulerPairCoordinates_injective {F : Type u_1} [Field F] (k : ℕ) : Function.Injective ⇑(eulerPairCoordinates F k)

Over a field, the map (A, B, Q) ↦ (A + y * Q, B - x * Q) is injective.

theorem CCDN.finrank_eulerPairSpace {F : Type u_1} [Field F] (k : ℕ) : Module.finrank F (EulerPairSpace F k) = (k + 2) ^ 2 - 1

The number of unknowns is exactly the desired Noether-form degree.