Canonical monomial coordinates for the d^2-1 Euler parameters and the coefficient matrix of their closed-form operator.

@[reducible, inline]

abbrev CCDN.EulerLowIndex (k : ℕ) : Type

Index set of the bivariate monomials of total degree at most k, encoded as multisets of size k in Option (Fin 2) (the entry none pads the degree up to k).

Equations

• CCDN.EulerLowIndex k = Sym (Option (Fin 2)) k

@[reducible, inline]

abbrev CCDN.EulerTopIndex (k : ℕ) : Type

Index set of the bivariate monomials of total degree exactly k, encoded as multisets of size k in Fin 2.

Equations

• CCDN.EulerTopIndex k = Sym (Fin 2) k

@[reducible, inline]

abbrev CCDN.EulerColumns (k : ℕ) : Type

Index set of the basis eulerPairBasis of EulerPairSpace R k: two blocks of monomials of degree at most k and one block of monomials of degree exactly k. These index the columns of the Euler closed-form coefficient matrix.

Equations

• CCDN.EulerColumns k = (CCDN.EulerLowIndex k ⊕ CCDN.EulerLowIndex k ⊕ CCDN.EulerTopIndex k)

noncomputable def CCDN.eulerLowBasis (R : Type u_1) [CommRing R] (k : ℕ) : Module.Basis (EulerLowIndex k) R ↥(MvPolynomial.restrictTotalDegree (Fin 2) R k)

The usual monomial basis of the total-degree-at-most space.

Equations

• CCDN.eulerLowBasis R k = (MvPolynomial.basisRestrictSupport R {p : Fin 2 →₀ ℕ | Finsupp.degree p ≤ k}).reindex (Finsupp.degreeLeEquivSym (Fin 2) k)

noncomputable def CCDN.eulerTopBasis (R : Type u_1) [CommRing R] (k : ℕ) : Module.Basis (EulerTopIndex k) R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R k)

The usual monomial basis of the homogeneous space.

Equations

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

noncomputable def CCDN.eulerPairBasis (R : Type u_1) [CommRing R] (k : ℕ) : Module.Basis (EulerColumns k) R (EulerPairSpace R k)

The monomial basis of EulerPairSpace R k. Under eulerPairCoordinates, every basis vector is either a single low monomial or one radial syzygy pair (yQ,-xQ); no coefficient-dependent basis is chosen.

Equations

• CCDN.eulerPairBasis R k = (CCDN.eulerLowBasis R k).prod ((CCDN.eulerLowBasis R k).prod (CCDN.eulerTopBasis R k))

theorem CCDN.card_eulerColumns (k : ℕ) : Fintype.card (EulerColumns k) = (k + 2) ^ 2 - 1

There are exactly (k + 2) ^ 2 - 1 Euler columns.

noncomputable def CCDN.eulerClosedFormCoefficientMatrix {R : Type u_1} [CommRing R] (k : ℕ) (f : Polynomial (Polynomial R)) : Matrix (ℕ × ℕ) (EulerColumns k) R

The matrix of the Euler closed-form operator of f in the basis eulerPairBasis. The equation's coefficients enter the matrix linearly. The column set has cardinality d^2-1, and rows are ordinary coefficient positions.

Equations

• CCDN.eulerClosedFormCoefficientMatrix k f i j = (((CCDN.eulerClosedFormOperator k f) ((CCDN.eulerPairBasis R k) j)).coeff i.1).coeff i.2

theorem CCDN.eulerClosedFormCoefficientMatrix_columns_independent {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] (k : ℕ) (f : Polynomial (Polynomial F)) (hf : Irreducible f) (a : F) (ha : a ≠ 0) (hl : f.leadingCoeff = Polynomial.C a) (hdeg : f.natDegree = k + 2) : LinearIndependent F (eulerClosedFormCoefficientMatrix k f).col

Linear independence of all d^2-1 coefficient columns for an irreducible equation with constant outer leading coefficient.