Degrees, homogeneous components and dimensions of homogeneous submodules

Main results

• MvPolynomial.homogeneousComponent_mul_of_isHomogeneous_left: multiplication by a homogeneous polynomial of degree d shifts homogeneous components by d.
• MvPolynomial.finrank_homogeneousSubmodule: over a field, the homogeneous polynomials of degree n in finitely many variables σ form a space of dimension (Fintype.card σ + n - 1).choose n.
• MvPolynomial.finrank_homogeneousSubmodule_fin: the same count for n + 1 variables, in the form (n + M).choose M.
• Sym.equivNatSumLeOfFintype, Finsupp.degreeLeEquivSym: exponent vectors of degree at most n on α are multisets of size n on Option α.
• MvPolynomial.finrank_restrictTotalDegree: over a field, the polynomials of total degree at most N in finitely many variables σ form a space of dimension (Fintype.card σ + N).choose N.
• MvPolynomial.degreeOf_aeval_le: substituting polynomials of degree at most D in a variable i into f gives degree at most D * f.totalDegree in i. Since each matrix entry occurs to degree at most one in every maximal minor, substituting maximal minors preserves a degree bound in every individual matrix coordinate.
• MvPolynomial.totalDegree_map_of_injective: mapping coefficients along an injective ring homomorphism preserves the total degree.
• MvPolynomial.totalDegree_pos_of_ne_zero_of_not_isUnit: over a field, a nonzero nonunit has positive total degree.
• MvPolynomial.homogeneousComponent_totalDegree_ne_zero: the homogeneous component of top degree of a nonzero polynomial is nonzero.

noncomputable def Sym.equivNatSumLeOfFintype (α : Type u_1) [DecidableEq α] [Fintype α] (n : ℕ) : Sym (Option α) n ≃ { P : α → ℕ // ∑ i : α, P i ≤ n }

Multisets of size n on Option α correspond to functions α → ℕ with sum at most n; the multiplicity of none records the slack.

Equations

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

noncomputable def Finsupp.degreeLeEquivSym (α : Type u_1) [DecidableEq α] [Fintype α] (n : ℕ) : { P : α →₀ ℕ // degree P ≤ n } ≃ Sym (Option α) n

Exponent vectors of degree at most n on a finite type α correspond to multisets of size n on Option α.

Equations

• Finsupp.degreeLeEquivSym α n = (Finsupp.equivFunOnFinite.subtypeEquiv ⋯).trans (Sym.equivNatSumLeOfFintype α n).symm

theorem MvPolynomial.totalDegree_map_le {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) (p : MvPolynomial σ R) : ((map f) p).totalDegree ≤ p.totalDegree

Mapping coefficients never increases the total degree.

theorem MvPolynomial.totalDegree_map_of_injective {σ : Type u_1} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : MvPolynomial σ R) : ((map f) p).totalDegree = p.totalDegree

Mapping coefficients along an injective ring homomorphism preserves the total degree.

theorem MvPolynomial.totalDegree_pos_of_ne_zero_of_not_isUnit {σ : Type u_1} {K : Type u_2} [Field K] {f : MvPolynomial σ K} (hf : f ≠ 0) (hu : ¬IsUnit f) : 0 < f.totalDegree

Over a field, a nonzero polynomial which is not a unit has positive total degree.

theorem MvPolynomial.totalDegree_pos_of_irreducible {σ : Type u_1} {K : Type u_2} [Field K] {f : MvPolynomial σ K} (hf : Irreducible f) : 0 < f.totalDegree

Over a field, an irreducible polynomial has positive total degree.

theorem MvPolynomial.homogeneousComponent_totalDegree_ne_zero {σ : Type u_1} {R : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} (hp : p ≠ 0) : (homogeneousComponent p.totalDegree) p ≠ 0

The homogeneous component of top degree of a nonzero polynomial is nonzero.

theorem MvPolynomial.homogeneousComponent_mul_of_isHomogeneous_left {σ : Type u_1} {K : Type u_2} [CommRing K] {f : MvPolynomial σ K} {d : ℕ} (hf : f.IsHomogeneous d) (u : MvPolynomial σ K) (k : ℕ) : (homogeneousComponent (d + k)) (f * u) = f * (homogeneousComponent k) u

Multiplication by a homogeneous polynomial of degree d shifts homogeneous components by d.

theorem MvPolynomial.finrank_homogeneousSubmodule {σ : Type u_1} {K : Type u_2} [Field K] [Fintype σ] (n : ℕ) : Module.finrank K ↥(homogeneousSubmodule σ K n) = (Fintype.card σ + n - 1).choose n

The homogeneous polynomials of degree n in finitely many variables σ form a space of dimension (Fintype.card σ + n - 1).choose n, the number of monomials of degree n.

theorem MvPolynomial.finrank_restrictTotalDegree {σ : Type u_1} {K : Type u_2} [Field K] [Fintype σ] (N : ℕ) : Module.finrank K ↥(restrictTotalDegree σ K N) = (Fintype.card σ + N).choose N

The polynomials of total degree at most N in finitely many variables σ form a space of dimension (Fintype.card σ + N).choose N, the number of monomials of degree at most N.

theorem MvPolynomial.finrank_homogeneousSubmodule_fin {K : Type u_2} [Field K] (n M : ℕ) : Module.finrank K ↥(homogeneousSubmodule (Fin (n + 1)) K M) = (n + M).choose M

The homogeneous polynomials of degree M in n + 1 variables form a space of dimension (n + M).choose M.

theorem MvPolynomial.degreeOf_aeval_le {K : Type u_3} {σ : Type u_4} {τ : Type u_5} [Field K] [Finite σ] (a : σ → MvPolynomial τ K) (i : τ) (D : ℕ) (ha : ∀ (j : σ), degreeOf i (a j) ≤ D) (f : MvPolynomial σ K) : degreeOf i ((aeval a) f) ≤ D * f.totalDegree

Substituting polynomials of degree at most D in the variable i into f gives a polynomial of degree at most D * f.totalDegree in i.