A homogeneous form with independent integer coefficient variables, and its exact specialization to every homogeneous equation.

noncomputable def CCDN.homogeneousCoefficientExponent (σ : Type u_1) [Fintype σ] [DecidableEq σ] (d : ℕ) (i : Sym σ d) : σ →₀ ℕ

The exponent vector of degree d in the variables σ corresponding to a multiset i of size d.

Equations

• CCDN.homogeneousCoefficientExponent σ d i = ↑((CCDN.degreeEqEquivSym σ d).symm i)

theorem CCDN.homogeneousCoefficientExponent_degree (σ : Type u_1) [Fintype σ] [DecidableEq σ] (d : ℕ) (i : Sym σ d) : Finsupp.degree (homogeneousCoefficientExponent σ d i) = d

The exponent vector homogeneousCoefficientExponent σ d i has degree d.

noncomputable def CCDN.universalHomogeneousForm (σ : Type u_1) [Fintype σ] [DecidableEq σ] (d : ℕ) : MvPolynomial σ (MvPolynomial (Sym σ d) ℤ)

The universal homogeneous form of degree d in the variables σ: the sum of all monomials of degree d, each with its own independent integer coefficient variable.

Equations

• CCDN.universalHomogeneousForm σ d = ∑ i : Sym σ d, (MvPolynomial.monomial (CCDN.homogeneousCoefficientExponent σ d i)) (MvPolynomial.X i)

noncomputable def CCDN.homogeneousCoefficientData {R : Type u_1} {σ : Type u_2} [CommRing R] [Fintype σ] [DecidableEq σ] (d : ℕ) (f : MvPolynomial σ R) (i : Sym σ d) : R

The coefficient of f at the degree-d monomial indexed by i.

Equations

• CCDN.homogeneousCoefficientData d f i = f.coeff (CCDN.homogeneousCoefficientExponent σ d i)

theorem CCDN.homogeneousCoefficientData_reconstruct {R : Type u_1} {σ : Type u_2} [CommRing R] [Fintype σ] [DecidableEq σ] (d : ℕ) (f : MvPolynomial σ R) (hf : f.IsHomogeneous d) : ∑ i : Sym σ d, (MvPolynomial.monomial (homogeneousCoefficientExponent σ d i)) (homogeneousCoefficientData d f i) = f

A homogeneous polynomial f of degree d is the sum of its degree-d monomials weighted by homogeneousCoefficientData d f.

noncomputable def CCDN.homogeneousCoefficientSpecialization {R : Type u_1} {σ : Type u_2} [CommRing R] [Fintype σ] [DecidableEq σ] (d : ℕ) (f : MvPolynomial σ R) : MvPolynomial (Sym σ d) ℤ →+* R

The ring homomorphism from the integer polynomials in the coefficient variables to R that sends each coefficient variable to the corresponding coefficient of f.

Equations

• CCDN.homogeneousCoefficientSpecialization d f = MvPolynomial.eval₂Hom (Int.castRingHom R) (CCDN.homogeneousCoefficientData d f)

theorem CCDN.universalHomogeneousForm_specialize {R : Type u_1} {σ : Type u_2} [CommRing R] [Fintype σ] [DecidableEq σ] (d : ℕ) (f : MvPolynomial σ R) (hf : f.IsHomogeneous d) : (MvPolynomial.map (homogeneousCoefficientSpecialization d f)) (universalHomogeneousForm σ d) = f

The coefficient variables specialize to the homogeneous equation, over every commutative coefficient ring.

theorem CCDN.universalHomogeneousForm_linear_expansion (σ : Type u_1) [Fintype σ] [DecidableEq σ] (d : ℕ) : universalHomogeneousForm σ d = ∑ i : Sym σ d, MvPolynomial.X i • (MvPolynomial.map MvPolynomial.C) ((MvPolynomial.monomial (homogeneousCoefficientExponent σ d i)) 1)

The universal homogeneous form is the sum over all degree-d monomials of the coefficient variable times that monomial, an expansion linear in the coefficient variables.

noncomputable def CCDN.universalPlanePolynomialLinear (R : Type u_1) (σ : Type u_2) [CommRing R] : MvPolynomial σ R →ₗ[R] Polynomial (Polynomial (MvPolynomial (PlaneParameters σ) R))

The universal plane restriction universalPlanePolynomial as an R-linear map.

Equations

• CCDN.universalPlanePolynomialLinear R σ = ↑R (CCDN.bivariatePolynomialEquiv (MvPolynomial (CCDN.PlaneParameters σ) R)).toLinearMap ∘ₗ (CCDN.universalPlaneMap R σ).toLinearMap