Complete homogeneous monomial lists, their exact cardinalities, and the corresponding polynomial-space dimensions.

noncomputable def CCDN.degreeEqEquivSym (σ : Type u_1) [Fintype σ] [DecidableEq σ] (M : ℕ) : { p : σ →₀ ℕ // Finsupp.degree p = M } ≃ Sym σ M

Exponents of total degree exactly M are multisets of cardinality M.

Equations

• CCDN.degreeEqEquivSym σ M = (Finsupp.equivFunOnFinite.subtypeEquiv ⋯).trans (Sym.equivNatSumOfFintype σ M).symm

theorem CCDN.card_degree_eq (n M : ℕ) : Nat.card { p : Fin (n + 1) →₀ ℕ // Finsupp.degree p = M } = (n + M).choose M

There are exactly (n + M).choose M exponent vectors of total degree M in n + 1 variables.

noncomputable def CCDN.homogeneousExponentEquiv (n M : ℕ) : Fin ((n + M).choose M) ≃ { p : Fin (n + 1) →₀ ℕ // Finsupp.degree p = M }

A canonical finite indexing of all degree-M monomials in n+1 variables.

Equations

• CCDN.homogeneousExponentEquiv n M = (finCongr ⋯).trans (Fintype.equivFin { p : Fin (n + 1) →₀ ℕ // Finsupp.degree p = M }).symm

noncomputable def CCDN.homogeneousMonomials (n M : ℕ) : Fin ((n + M).choose M) → Fin (n + 1) →₀ ℕ

The list of all exponent vectors of total degree M in n + 1 variables, indexed by Fin ((n + M).choose M) via homogeneousExponentEquiv.

Equations

• CCDN.homogeneousMonomials n M j = ↑((CCDN.homogeneousExponentEquiv n M) j)

theorem CCDN.homogeneousMonomials_injective (n M : ℕ) : Function.Injective (homogeneousMonomials n M)

Distinct indices give distinct monomials in homogeneousMonomials n M.

theorem CCDN.homogeneousMonomials_degree (n M : ℕ) (j : Fin ((n + M).choose M)) : Finsupp.degree (homogeneousMonomials n M j) = M

Every monomial in homogeneousMonomials n M has total degree M.

theorem CCDN.homogeneousMonomials_surjective (n M : ℕ) (p : Fin (n + 1) →₀ ℕ) (hp : Finsupp.degree p = M) : ∃ (j : Fin ((n + M).choose M)), homogeneousMonomials n M j = p

Every exponent vector of total degree M in n + 1 variables occurs in homogeneousMonomials n M.

theorem CCDN.polynomialOfCoefficients_homogeneous (n M : ℕ) (v : Fin ((n + M).choose M) → ℤ) : (polynomialOfCoefficients (homogeneousMonomials n M) v).IsHomogeneous M

An integer combination of the degree-M monomials homogeneousMonomials n M is a homogeneous polynomial of degree M.