Leading monomials for a monomial order

This file collects facts about leading monomials of multivariate polynomials for a monomial order m on σ →₀ ℕ: comparisons of degrees with their WithBot forms, the degree of a monomial multiple, the cancellation of leading terms by an S-polynomial, the behaviour of leading data under a change of coefficients, leading data of the weighted homogeneous component containing the leading monomial, the top weighted part of a binomial lifted by terms of lower weight, leading data of renamed polynomials, elimination orders and the lexicographic ones among them, agreement of leading exponents under two monomial orders, leading data for nonnegative weight refinements, normalization to leading coefficient one over a field, leading exponents of substitutions of nonzero families, leading data of substitutions of monic families, cancellation of substituted monic binomials, and algebraic independence from leading monomials.

The product X^a * b, normalized to leading coefficient one when b has a unit leading coefficient, differs from another such product of the same degree by a monomial multiple of their S-polynomial. This is the cancellation of leading terms behind Buchberger's criterion.

Let yᵢ, i ∈ σ, be polynomials in the variables Xᵢ over a ring without zero divisors. If the leading monomial of each yᵢ is the variable Xᵢ, then the yᵢ are algebraically independent: the image of a monomial c X^d under Xᵢ ↦ yᵢ has leading monomial X^d, so the images of the distinct monomials of a nonzero polynomial have distinct leading monomials and cannot cancel.

This is the triangularity argument for a family such as yₙ = cₙ Xₙ + qₙ(X₁, …, Xₙ₋₁) with cₙ ≠ 0, ordered lexicographically with the variables of larger index more significant, as for the images of the generators of the Lazard ring in a polynomial ring.

Main results

• MonomialOrder.degree_eq_of_forall_lt, MonomialOrder.degree_eq_of_forall_mem_lt: strict comparisons preserving the leading exponent, including comparisons on a set containing the support and original leading exponent.
• MonomialOrder.leadingCoeff_eq_of_degree_eq, MonomialOrder.leadingTerm_eq_of_degree_eq, MonomialOrder.sPolynomial_eq_of_degree_eq: orders agreeing on leading exponents also agree on the corresponding leading coefficients, leading terms and S-polynomials.
• MonomialOrder.toWithBotSyn_withBotDegree_le_toSyn_degree: the WithBot degree of a polynomial is at most its degree.
• MonomialOrder.withBotDegree_sub_lt: if q has degree at most that of f ≠ 0 and the same coefficient of X^(deg f), then f - q has smaller degree than f.
• MvPolynomial.monomial_mem_iff_monomial_one_mem: a set closed under scalar multiplication contains c X^a for a unit c if and only if it contains X^a.
• MonomialOrder.leadingTerm_mem_iff: a set closed under scalar multiplication contains the leading term of a polynomial with unit leading coefficient if and only if it contains its leading monomial.
• MonomialOrder.toSyn_degree_monomial_mul_le: c X^a * b has degree at most a + deg b.
• MonomialOrder.monomial_one_mul_sub_smul_eq_monomial_mul_sPolynomial: if b₀ has a unit leading coefficient, then X^a * b minus lc b times the product of b₀ of the same degree normalized to leading coefficient one is a monomial multiple of the S-polynomial m.sPolynomial b b₀.
• MonomialOrder.degree_map_of_injective, MonomialOrder.leadingCoeff_map_of_injective, MonomialOrder.leadingTerm_map_of_injective, MonomialOrder.sPolynomial_map_of_injective: an injective coefficient map φ preserves leading monomials and commutes with leading coefficients, leading terms and S-polynomials.
• MonomialOrder.leadingTerm_weightedHomogeneousComponent_weight_degree: the weighted homogeneous component of f containing its leading monomial has the leading term of f.
• MonomialOrder.weightedHomogeneousComponent_monomial_sub_monomial_sub, MonomialOrder.linearCombination_le_of_mem_support_monomial_sub_monomial_sub: for weights A w = ∑ i, w i • a i, if A u = A v and all exponents w of Q satisfy A w ≺ A u, then the part of Y^u - Y^v - Q of weight A u is Y^u - Y^v, and all its exponents w satisfy A w ≼ A u.
• MonomialOrder.degree_rename, MonomialOrder.leadingCoeff_rename and MonomialOrder.leadingTerm_rename: renaming the variables along a relabeling which carries one monomial order to another commutes with leading monomials, coefficients and terms; such a relabeling is injective by MonomialOrder.injective_of_forall_toSyn_le_iff.
• MonomialOrder.exists_rename_eq_of_coe_support_degree_subset: for an elimination order, a polynomial whose leading monomial only involves the variables e τ is a renamed polynomial.
• MonomialOrder.coe_support_subset_of_lex_le: monomials supported in an upper set of variables form a lower set for the lexicographic order.
• MonomialOrder.weight_degree_weightRefinement: the refined leading exponent has maximal weight. MonomialOrder.degree_weightRefinement, MonomialOrder.leadingCoeff_weightRefinement and MonomialOrder.leadingTerm_weightRefinement identify its leading data with those of the maximal-weight component in the original order.
• MonomialOrder.monicNormalize: over a field, a polynomial divided by its leading coefficient, monic with the same leading exponent when the polynomial is nonzero (MonomialOrder.monic_monicNormalize, MonomialOrder.degree_monicNormalize).
• MonomialOrder.monic_aeval_monomial_one, MonomialOrder.degree_aeval_monomial_one: for a family c of monic polynomials, ∏ i, c i ^ w i is monic with leading exponent A w = ∑ i, w i • m.degree (c i).
• MonomialOrder.coeff_aeval_of_forall_le, MonomialOrder.degree_aeval_le_of_forall_le: if all exponents w of P have A w ≼ e, then the coefficient of X^e in aeval c P is the sum of the coefficients of P at the w with A w = e, and aeval c P has leading exponent at most e.
• MonomialOrder.algebraicIndependent_of_degree_eq_single: polynomials yᵢ whose leading monomial is Xᵢ are algebraically independent.

theorem MvPolynomial.monomial_mem_iff_monomial_one_mem {σ : Type u_1} {R : Type u_2} {S : Type u_3} [CommSemiring R] [SetLike S (MvPolynomial σ R)] [SMulMemClass S R (MvPolynomial σ R)] {a : σ →₀ ℕ} {c : R} (C : S) (hc : IsUnit c) : (monomial a) c ∈ C ↔ (monomial a) 1 ∈ C

A set of polynomials closed under scalar multiplication (for example a submodule or a subalgebra) contains a monomial with unit coefficient if and only if it contains the corresponding monomial with coefficient one.

theorem MonomialOrder.degree_eq_of_forall_lt {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (n : MonomialOrder σ) (f : MvPolynomial σ R) (h : ∀ a ∈ f.support, a ≠ m.degree f → n.toSyn a < n.toSyn (m.degree f)) : n.degree f = m.degree f

Two monomial orders give the same leading exponent of f if every other exponent in its support remains strictly below its original leading exponent.

theorem MonomialOrder.degree_eq_of_forall_mem_lt {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (n : MonomialOrder σ) (f : MvPolynomial σ R) {s : Set (σ →₀ ℕ)} (h : ∀ a ∈ s, ∀ b ∈ s, m.toSyn a < m.toSyn b → n.toSyn a < n.toSyn b) (hf : ↑f.support ⊆ s) (hd : m.degree f ∈ s) : n.degree f = m.degree f

Orders preserving strict comparisons on a set containing the support and original leading exponent of a polynomial give it the same leading exponent.

theorem MonomialOrder.leadingCoeff_eq_of_degree_eq {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (n : MonomialOrder σ) {f : MvPolynomial σ R} (h : n.degree f = m.degree f) : n.leadingCoeff f = m.leadingCoeff f

Orders agreeing on the leading exponent of a polynomial agree on its leading coefficient.

theorem MonomialOrder.leadingTerm_eq_of_degree_eq {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (n : MonomialOrder σ) {f : MvPolynomial σ R} (h : n.degree f = m.degree f) : n.leadingTerm f = m.leadingTerm f

Orders agreeing on the leading exponent of a polynomial agree on its leading term.

theorem MonomialOrder.sPolynomial_eq_of_degree_eq {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommRing R] (n : MonomialOrder σ) {f g : MvPolynomial σ R} (hf : n.degree f = m.degree f) (hg : n.degree g = m.degree g) : n.sPolynomial f g = m.sPolynomial f g

Orders agreeing on the leading exponents of two polynomials give the same S-polynomial.

theorem MonomialOrder.toWithBotSyn_withBotDegree_le_toSyn_degree {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (p : MvPolynomial σ R) : m.toWithBotSyn (m.withBotDegree p) ≤ ↑(m.toSyn (m.degree p))

The WithBot degree of a polynomial is at most its degree.

theorem MonomialOrder.withBotDegree_sub_lt {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommRing R] {f q : MvPolynomial σ R} (hf : f ≠ 0) (hq : m.toWithBotSyn (m.withBotDegree q) ≤ m.toWithBotSyn (m.withBotDegree f)) (hqf : q.coeff (m.degree f) = m.leadingCoeff f) : m.toWithBotSyn (m.withBotDegree (f - q)) < m.toWithBotSyn (m.withBotDegree f)

If q has degree at most that of f ≠ 0 and the same coefficient of X^(deg f), then f - q has smaller degree than f.

theorem MonomialOrder.degree_sub_lt {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommRing R] {f q : MvPolynomial σ R} (hfq : f - q ≠ 0) (hq : m.toSyn (m.degree q) ≤ m.toSyn (m.degree f)) (hqf : q.coeff (m.degree f) = m.leadingCoeff f) : m.toSyn (m.degree (f - q)) < m.toSyn (m.degree f)

If q has degree at most that of f and the same coefficient of X^(deg f), then f - q has strictly smaller leading exponent when the difference is nonzero.

theorem MonomialOrder.toSyn_degree_monomial_mul_le {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (a : σ →₀ ℕ) (c : R) (b : MvPolynomial σ R) : m.toSyn (m.degree ((MvPolynomial.monomial a) c * b)) ≤ m.toSyn (a + m.degree b)

A monomial multiple c X^a * b has degree at most a + deg b.

theorem MonomialOrder.leadingTerm_mem_iff {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] {S : Type u_3} [SetLike S (MvPolynomial σ R)] [SMulMemClass S R (MvPolynomial σ R)] {f : MvPolynomial σ R} (C : S) (hf : IsUnit (m.leadingCoeff f)) : m.leadingTerm f ∈ C ↔ (MvPolynomial.monomial (m.degree f)) 1 ∈ C

A set of polynomials closed under scalar multiplication (for example a submodule or a subalgebra) contains the leading term of a polynomial with unit leading coefficient if and only if it contains its leading monomial.

theorem MonomialOrder.monomial_one_mul_sub_smul_eq_monomial_mul_sPolynomial {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommRing R] {a : σ →₀ ℕ} {b b₀ : MvPolynomial σ R} (hb₀ : m.degree b₀ ≤ a + m.degree b) (u₀ : Rˣ) (hu₀ : ↑u₀ = m.leadingCoeff b₀) : (MvPolynomial.monomial a) 1 * b - m.leadingCoeff b • ((MvPolynomial.monomial (a + m.degree b - m.degree b₀)) ↑u₀⁻¹ * b₀) = (MvPolynomial.monomial (a + m.degree b - m.degree b ⊔ m.degree b₀)) ↑u₀⁻¹ * m.sPolynomial b b₀

Cancellation of leading terms by an S-polynomial. If b₀ has unit leading coefficient u₀ and deg b₀ ≤ a + deg b, the difference between X^a * b and lc b times the normalized product X^(a + deg b - deg b₀) * b₀ / lc b₀ is X^(a + deg b - L) / lc b₀ * S(b, b₀), where L = deg b ⊔ deg b₀.

theorem MonomialOrder.degree_map_of_leadingCoeff_ne_zero {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {S : Type u_3} [CommSemiring R] [CommSemiring S] (φ : R →+* S) {f : MvPolynomial σ R} (h : φ (m.leadingCoeff f) ≠ 0) : m.degree ((MvPolynomial.map φ) f) = m.degree f

A coefficient map that does not kill the leading coefficient preserves the leading monomial.

theorem MonomialOrder.leadingCoeff_map_of_leadingCoeff_ne_zero {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {S : Type u_3} [CommSemiring R] [CommSemiring S] (φ : R →+* S) {f : MvPolynomial σ R} (h : φ (m.leadingCoeff f) ≠ 0) : m.leadingCoeff ((MvPolynomial.map φ) f) = φ (m.leadingCoeff f)

A coefficient map that does not kill the leading coefficient maps it to the leading coefficient of the image.

theorem MonomialOrder.degree_map_of_injective {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {S : Type u_3} [CommSemiring R] [CommSemiring S] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (f : MvPolynomial σ R) : m.degree ((MvPolynomial.map φ) f) = m.degree f

An injective coefficient map preserves the leading monomial.

theorem MonomialOrder.withBotDegree_map_of_injective {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {S : Type u_3} [CommSemiring R] [CommSemiring S] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (f : MvPolynomial σ R) : m.withBotDegree ((MvPolynomial.map φ) f) = m.withBotDegree f

An injective coefficient map preserves the WithBot degree.

theorem MonomialOrder.leadingCoeff_map_of_injective {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {S : Type u_3} [CommSemiring R] [CommSemiring S] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (f : MvPolynomial σ R) : m.leadingCoeff ((MvPolynomial.map φ) f) = φ (m.leadingCoeff f)

An injective coefficient map sends the leading coefficient to the leading coefficient of the image.

theorem MonomialOrder.leadingTerm_map_of_injective {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {S : Type u_3} [CommSemiring R] [CommSemiring S] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (f : MvPolynomial σ R) : m.leadingTerm ((MvPolynomial.map φ) f) = (MvPolynomial.map φ) (m.leadingTerm f)

An injective coefficient map sends the leading term to the leading term of the image.

theorem MonomialOrder.sPolynomial_map_of_injective {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {S : Type u_3} [CommRing R] [CommRing S] {φ : R →+* S} (hφ : Function.Injective ⇑φ) (f g : MvPolynomial σ R) : m.sPolynomial ((MvPolynomial.map φ) f) ((MvPolynomial.map φ) g) = (MvPolynomial.map φ) (m.sPolynomial f g)

An injective coefficient map sends the S-polynomial of f and g to the S-polynomial of their images.

@[simp]

theorem MonomialOrder.degree_weightedHomogeneousComponent_weight_degree {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {M : Type u_3} [AddCommMonoid M] [CommSemiring R] (w : σ → M) (f : MvPolynomial σ R) : m.degree ((MvPolynomial.weightedHomogeneousComponent w ((Finsupp.weight w) (m.degree f))) f) = m.degree f

The weighted homogeneous component of f whose weight is that of the leading monomial of f has the same leading monomial as f.

@[simp]

theorem MonomialOrder.leadingCoeff_weightedHomogeneousComponent_weight_degree {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {M : Type u_3} [AddCommMonoid M] [CommSemiring R] (w : σ → M) (f : MvPolynomial σ R) : m.leadingCoeff ((MvPolynomial.weightedHomogeneousComponent w ((Finsupp.weight w) (m.degree f))) f) = m.leadingCoeff f

The weighted homogeneous component of f containing its leading monomial has the same leading coefficient as f.

@[simp]

theorem MonomialOrder.leadingTerm_weightedHomogeneousComponent_weight_degree {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {M : Type u_3} [AddCommMonoid M] [CommSemiring R] (w : σ → M) (f : MvPolynomial σ R) : m.leadingTerm ((MvPolynomial.weightedHomogeneousComponent w ((Finsupp.weight w) (m.degree f))) f) = m.leadingTerm f

The weighted homogeneous component of f containing its leading monomial has the same leading term as f.

theorem MonomialOrder.isWeightedHomogeneous_weightedHomogeneousComponent_weight_degree {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) {M : Type u_3} [AddCommMonoid M] [CommSemiring R] (w : σ → M) (f : MvPolynomial σ R) : MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.weightedHomogeneousComponent w ((Finsupp.weight w) (m.degree f))) f) ((Finsupp.weight w) (m.degree ((MvPolynomial.weightedHomogeneousComponent w ((Finsupp.weight w) (m.degree f))) f)))

The weighted homogeneous component of f containing its leading monomial is weighted homogeneous of the weight of its own leading monomial.

@[simp]

theorem MonomialOrder.weight_degree_weightRefinement {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (w : σ → ℕ) (f : MvPolynomial σ R) : (Finsupp.weight w) ((m.weightRefinement w).degree f) = MvPolynomial.weightedTotalDegree w f

The leading exponent for a weight-refined order has maximal weight. This includes the zero polynomial, whose degree and weighted total degree are both totalized at zero.

theorem MonomialOrder.degree_weightRefinement_of_isWeightedHomogeneous {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (w : σ → ℕ) {f : MvPolynomial σ R} {d : ℕ} (hf : MvPolynomial.IsWeightedHomogeneous w f d) : (m.weightRefinement w).degree f = m.degree f

Refining by weight does not change the leading exponent of a weighted homogeneous polynomial: all comparisons in its support are ties in weight.

theorem MonomialOrder.degree_weightRefinement {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (w : σ → ℕ) (f : MvPolynomial σ R) : (m.weightRefinement w).degree f = m.degree ((MvPolynomial.weightedHomogeneousComponent w (MvPolynomial.weightedTotalDegree w f)) f)

The refined leading exponent is the original-order leading exponent of the maximal-weight component. This is the polynomial comparison underlying refinement of weight initials.

theorem MonomialOrder.leadingCoeff_weightRefinement {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (w : σ → ℕ) (f : MvPolynomial σ R) : (m.weightRefinement w).leadingCoeff f = m.leadingCoeff ((MvPolynomial.weightedHomogeneousComponent w (MvPolynomial.weightedTotalDegree w f)) f)

The leading coefficient for a weight-refined order is the leading coefficient, in the original order, of the maximal-weight component.

theorem MonomialOrder.leadingTerm_weightRefinement {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (w : σ → ℕ) (f : MvPolynomial σ R) : (m.weightRefinement w).leadingTerm f = m.leadingTerm ((MvPolynomial.weightedHomogeneousComponent w (MvPolynomial.weightedTotalDegree w f)) f)

The leading term for a weight-refined order is the leading term, in the original order, of the maximal-weight component. In particular, tied maximal-weight terms are not discarded until the original monomial order is applied.

@[simp]

theorem MonomialOrder.degree_weightRefinement_zero {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] (f : MvPolynomial σ R) : (m.weightRefinement 0).degree f = m.degree f

Zero-weight refinement leaves polynomial leading exponents unchanged.

theorem MonomialOrder.weightedHomogeneousComponent_monomial_sub_monomial_sub {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {ι : Type u_3} [CommRing R] {a : ι → σ →₀ ℕ} {u v : ι →₀ ℕ} {Q : MvPolynomial ι R} (huv : (Finsupp.linearCombination ℕ a) u = (Finsupp.linearCombination ℕ a) v) (hQ : ∀ w ∈ Q.support, m.toSyn ((Finsupp.linearCombination ℕ a) w) < m.toSyn ((Finsupp.linearCombination ℕ a) u)) : (MvPolynomial.weightedHomogeneousComponent a ((Finsupp.linearCombination ℕ a) u)) ((MvPolynomial.monomial u) 1 - (MvPolynomial.monomial v) 1 - Q) = (MvPolynomial.monomial u) 1 - (MvPolynomial.monomial v) 1

Let A w = ∑ i, w i • a i. If A u = A v and every exponent w of Q satisfies A w ≺ A u, then the part of the lifted relation Y^u - Y^v - Q of weight A u is the binomial Y^u - Y^v.

theorem MonomialOrder.linearCombination_le_of_mem_support_monomial_sub_monomial_sub {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {ι : Type u_3} [CommRing R] {a : ι → σ →₀ ℕ} {u v : ι →₀ ℕ} {Q : MvPolynomial ι R} (huv : (Finsupp.linearCombination ℕ a) u = (Finsupp.linearCombination ℕ a) v) (hQ : ∀ w ∈ Q.support, m.toSyn ((Finsupp.linearCombination ℕ a) w) < m.toSyn ((Finsupp.linearCombination ℕ a) u)) {w : ι →₀ ℕ} (hw : w ∈ ((MvPolynomial.monomial u) 1 - (MvPolynomial.monomial v) 1 - Q).support) : m.toSyn ((Finsupp.linearCombination ℕ a) w) ≤ m.toSyn ((Finsupp.linearCombination ℕ a) u)

Let A w = ∑ i, w i • a i. If A u = A v and every exponent w of Q satisfies A w ≺ A u, then every exponent w of the lifted relation Y^u - Y^v - Q satisfies A w ≼ A u: its part of weight A u is its top part.

theorem MonomialOrder.injective_of_forall_toSyn_le_iff {σ : Type u_1} {m : MonomialOrder σ} {τ : Type u_3} {m' : MonomialOrder τ} {e : τ → σ} (hm : ∀ (a b : τ →₀ ℕ), m'.toSyn a ≤ m'.toSyn b ↔ m.toSyn (Finsupp.mapDomain e a) ≤ m.toSyn (Finsupp.mapDomain e b)) : Function.Injective e

A relabeling of variables which carries the monomial order m' to m is injective.

theorem MonomialOrder.degree_rename {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {τ : Type u_3} [CommSemiring R] {m' : MonomialOrder τ} {e : τ → σ} (hm : ∀ (a b : τ →₀ ℕ), m'.toSyn a ≤ m'.toSyn b ↔ m.toSyn (Finsupp.mapDomain e a) ≤ m.toSyn (Finsupp.mapDomain e b)) (p : MvPolynomial τ R) : m.degree ((MvPolynomial.rename e) p) = Finsupp.mapDomain e (m'.degree p)

Renaming the variables along a relabeling which carries the monomial order m' to m renames the leading monomial.

theorem MonomialOrder.leadingCoeff_rename {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {τ : Type u_3} [CommSemiring R] {m' : MonomialOrder τ} {e : τ → σ} (hm : ∀ (a b : τ →₀ ℕ), m'.toSyn a ≤ m'.toSyn b ↔ m.toSyn (Finsupp.mapDomain e a) ≤ m.toSyn (Finsupp.mapDomain e b)) (p : MvPolynomial τ R) : m.leadingCoeff ((MvPolynomial.rename e) p) = m'.leadingCoeff p

Renaming the variables along a relabeling which carries the monomial order m' to m preserves the leading coefficient.

theorem MonomialOrder.leadingTerm_rename {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {τ : Type u_3} [CommSemiring R] {m' : MonomialOrder τ} {e : τ → σ} (hm : ∀ (a b : τ →₀ ℕ), m'.toSyn a ≤ m'.toSyn b ↔ m.toSyn (Finsupp.mapDomain e a) ≤ m.toSyn (Finsupp.mapDomain e b)) (p : MvPolynomial τ R) : m.leadingTerm ((MvPolynomial.rename e) p) = (MvPolynomial.rename e) (m'.leadingTerm p)

Renaming the variables along a relabeling which carries the monomial order m' to m renames the leading term.

theorem MonomialOrder.exists_rename_eq_of_coe_support_degree_subset {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {τ : Type u_3} [CommSemiring R] {e : τ → σ} (helim : ∀ (a b : σ →₀ ℕ), m.toSyn a ≤ m.toSyn b → ↑b.support ⊆ Set.range e → ↑a.support ⊆ Set.range e) (he : Function.Injective e) {g : MvPolynomial σ R} (hg : ↑(m.degree g).support ⊆ Set.range e) : ∃ (g' : MvPolynomial τ R), (MvPolynomial.rename e) g' = g

For an elimination order m for the variables e τ, that is, one in which every monomial below a monomial in these variables is again a monomial in these variables, a polynomial whose leading monomial only involves the variables e τ is the renaming of a polynomial in the variables τ.

theorem MonomialOrder.coe_support_subset_of_lex_le {σ : Type u_1} [LinearOrder σ] [WellFoundedGT σ] {s : Set σ} (hs : IsUpperSet s) {a b : σ →₀ ℕ} (hab : lex.toSyn a ≤ lex.toSyn b) (hb : ↑b.support ⊆ s) : ↑a.support ⊆ s

For the lexicographic order, the monomials supported in an upper set of variables form a lower set: with the antitone variable convention these are the smallest variables.

noncomputable def MonomialOrder.monicNormalize {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_3} [Field k] (f : MvPolynomial σ k) : MvPolynomial σ k

The polynomial f divided by its leading coefficient for the monomial order m. It is monic when f ≠ 0 (MonomialOrder.monic_monicNormalize), and 0 when f = 0.

theorem MonomialOrder.monicNormalize_def {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] (f : MvPolynomial σ k) : m.monicNormalize f = MvPolynomial.C (m.leadingCoeff f)⁻¹ * f

@[simp]

theorem MonomialOrder.monicNormalize_zero {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] : m.monicNormalize 0 = 0

@[simp]

theorem MonomialOrder.monicNormalize_eq_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] {f : MvPolynomial σ k} : m.monicNormalize f = 0 ↔ f = 0

@[simp]

theorem MonomialOrder.degree_monicNormalize {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] (f : MvPolynomial σ k) : m.degree (m.monicNormalize f) = m.degree f

Normalization does not change the leading exponent.

theorem MonomialOrder.monic_monicNormalize {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] {f : MvPolynomial σ k} (hf : f ≠ 0) : m.Monic (m.monicNormalize f)

@[simp]

theorem MonomialOrder.C_leadingCoeff_mul_monicNormalize {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] (f : MvPolynomial σ k) : MvPolynomial.C (m.leadingCoeff f) * m.monicNormalize f = f

Multiplying the normalization of f by the leading coefficient of f recovers f.

theorem MonomialOrder.Monic.monicNormalize_eq {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] {f : MvPolynomial σ k} (hf : m.Monic f) : m.monicNormalize f = f

A monic polynomial is its own normalization.

theorem MonomialOrder.leadingTerm_monicNormalize_of_ne_zero {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] {f : MvPolynomial σ k} (hf : f ≠ 0) : m.leadingTerm (m.monicNormalize f) = (MvPolynomial.monomial (m.degree f)) 1

The normalization of a nonzero polynomial has leading term X ^ (m.degree f).

theorem MonomialOrder.leadingTerm_monicNormalize {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] (f : MvPolynomial σ k) : m.leadingTerm (m.monicNormalize f) = m.monicNormalize (m.leadingTerm f)

The leading term of the normalization is the normalization of the leading term.

@[simp]

theorem MonomialOrder.monicNormalize_mem_iff {σ : Type u_1} {m : MonomialOrder σ} {k : Type u_3} [Field k] {f : MvPolynomial σ k} {S : Type u_4} [SetLike S (MvPolynomial σ k)] [SMulMemClass S k (MvPolynomial σ k)] {A : S} : m.monicNormalize f ∈ A ↔ f ∈ A

A set of polynomials closed under multiplication by scalars in k (for example a k-subalgebra or a k-submodule) contains the normalization of f if and only if it contains f.

theorem MvPolynomial.aeval_monomial_one_ne_zero {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Nontrivial R] [NoZeroDivisors R] {ι : Type u_3} {b : ι → MvPolynomial σ R} (hb : ∀ (i : ι), b i ≠ 0) (u : ι →₀ ℕ) : (aeval b) ((monomial u) 1) ≠ 0

Substituting nonzero polynomials into a coefficient-one monomial gives a nonzero polynomial over a nontrivial semiring without zero divisors.

theorem MonomialOrder.degree_aeval_monomial_one_of_ne_zero {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommSemiring R] [NoZeroDivisors R] {ι : Type u_3} {b : ι → MvPolynomial σ R} (hb : ∀ (i : ι), b i ≠ 0) (u : ι →₀ ℕ) : m.degree ((MvPolynomial.aeval b) ((MvPolynomial.monomial u) 1)) = (Finsupp.linearCombination ℕ (m.degree ∘ b)) u

Substituting nonzero polynomials into a coefficient-one monomial adds their leading exponents, with the multiplicities prescribed by the monomial.

theorem MonomialOrder.monic_aeval_monomial_one {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {ι : Type u_3} [CommSemiring R] {c : ι → MvPolynomial σ R} (hc : ∀ (i : ι), m.Monic (c i)) (w : ι →₀ ℕ) : m.Monic ((MvPolynomial.aeval c) ((MvPolynomial.monomial w) 1))

The image of the monomial Y^w under the substitution of a monic family is monic.

theorem MonomialOrder.degree_aeval_monomial_one {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {ι : Type u_3} [CommSemiring R] {c : ι → MvPolynomial σ R} [Nontrivial R] (hc : ∀ (i : ι), m.Monic (c i)) (w : ι →₀ ℕ) : m.degree ((MvPolynomial.aeval c) ((MvPolynomial.monomial w) 1)) = (Finsupp.linearCombination ℕ fun (i : ι) => m.degree (c i)) w

The image of the monomial Y^w under the substitution of a monic family c has leading exponent ∑ i, w i • m.degree (c i).

theorem MonomialOrder.coeff_aeval_of_forall_le {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {ι : Type u_3} [CommSemiring R] {c : ι → MvPolynomial σ R} [Nontrivial R] (hc : ∀ (i : ι), m.Monic (c i)) {P : MvPolynomial ι R} {e : σ →₀ ℕ} (hP : ∀ w ∈ P.support, m.toSyn ((Finsupp.linearCombination ℕ fun (i : ι) => m.degree (c i)) w) ≤ m.toSyn e) : ((MvPolynomial.aeval c) P).coeff e = ∑ w ∈ P.support with (Finsupp.linearCombination ℕ fun (i : ι) => m.degree (c i)) w = e, P.coeff w

Let c be a monic family and write A w = ∑ i, w i • m.degree (c i). If every exponent w of P satisfies A w ≼ e, then the coefficient of X^e in aeval c P is the sum of the coefficients of P at the exponents w with A w = e: the images of the other monomials of P have leading exponent below e.

theorem MonomialOrder.degree_aeval_le_of_forall_le {σ : Type u_1} {R : Type u_2} {m : MonomialOrder σ} {ι : Type u_3} [CommSemiring R] {c : ι → MvPolynomial σ R} [Nontrivial R] (hc : ∀ (i : ι), m.Monic (c i)) {P : MvPolynomial ι R} {e : σ →₀ ℕ} (hP : ∀ w ∈ P.support, m.toSyn ((Finsupp.linearCombination ℕ fun (i : ι) => m.degree (c i)) w) ≤ m.toSyn e) : m.toSyn (m.degree ((MvPolynomial.aeval c) P)) ≤ m.toSyn e

Let c be a monic family and write A w = ∑ i, w i • m.degree (c i). If every exponent w of P satisfies A w ≼ e, then aeval c P has leading exponent at most e.

theorem MonomialOrder.aeval_monomial_sub_monomial_eq_zero_or_degree_lt {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommRing R] {ι : Type u_3} {b : ι → MvPolynomial σ R} [Nontrivial R] (hb : ∀ (i : ι), m.Monic (b i)) (u v : ι →₀ ℕ) (huv : (Finsupp.linearCombination ℕ (m.degree ∘ b)) u = (Finsupp.linearCombination ℕ (m.degree ∘ b)) v) : (MvPolynomial.aeval b) ((MvPolynomial.monomial u) 1 - (MvPolynomial.monomial v) 1) = 0 ∨ m.toSyn (m.degree ((MvPolynomial.aeval b) ((MvPolynomial.monomial u) 1 - (MvPolynomial.monomial v) 1))) < m.toSyn ((Finsupp.linearCombination ℕ (m.degree ∘ b)) u)

The substituted value of a coefficient-one binomial relation of a monic family vanishes or has leading exponent strictly below the common exponent of its two terms.

theorem MonomialOrder.algebraicIndependent_of_degree_eq_single {σ : Type u_1} {R : Type u_2} (m : MonomialOrder σ) [CommRing R] [NoZeroDivisors R] {y : σ → MvPolynomial σ R} (hy : ∀ (i : σ), m.degree (y i) = Finsupp.single i 1) : AlgebraicIndependent R y

Algebraic independence from leading monomials. Over a ring without zero divisors, a family yᵢ of polynomials in the variables Xᵢ whose leading monomial for a monomial order is Xᵢ is algebraically independent.