Documentation

TauCeti.Data.Finsupp.MonomialOrder.Refinement

Weight refinements of monomial orders #

A nonnegative integral weight compares exponents only partially: distinct monomials can have the same weight. MonomialOrder.weightRefinement breaks these ties with a given monomial order. The resulting order is again a native MonomialOrder, even with zero weights and infinitely many variables. It can therefore be used with polynomial division and Gröbner bases, while retaining the maximal-weight convention for initial forms.

The construction embeds exponents into the lexicographic product of their weight and their original ordered exponent. Both factors are well ordered.

References #

source
noncomputable def MonomialOrder.weightRefinement {σ : Type u_1} (m : MonomialOrder σ) (w : σ → ℕ) :
MonomialOrder σ

Compare nonnegative integral weights first, breaking ties using m.

Instances For
    source
    theorem MonomialOrder.weightRefinement_le_iff {σ : Type u_1} (m : MonomialOrder σ) (w : σ → ℕ) {a b : σ →₀ ℕ} :
    (m.weightRefinement w).toSyn a ≤ (m.weightRefinement w).toSyn b ↔ (Finsupp.weight w) a < (Finsupp.weight w) b ∨ (Finsupp.weight w) a = (Finsupp.weight w) b ∧ m.toSyn a ≤ m.toSyn b

    The weak comparison in a weight refinement.

    source
    theorem MonomialOrder.weightRefinement_lt_iff {σ : Type u_1} (m : MonomialOrder σ) (w : σ → ℕ) {a b : σ →₀ ℕ} :
    (m.weightRefinement w).toSyn a < (m.weightRefinement w).toSyn b ↔ (Finsupp.weight w) a < (Finsupp.weight w) b ∨ (Finsupp.weight w) a = (Finsupp.weight w) b ∧ m.toSyn a < m.toSyn b

    The strict comparison in a weight refinement.

    source
    theorem MonomialOrder.weight_le_of_weightRefinement_le {σ : Type u_1} (m : MonomialOrder σ) (w : σ → ℕ) {a b : σ →₀ ℕ} (h : (m.weightRefinement w).toSyn a ≤ (m.weightRefinement w).toSyn b) :
    (Finsupp.weight w) a ≤ (Finsupp.weight w) b

    A comparison in the refined order never decreases weight.

    source
    theorem MonomialOrder.weightRefinement_lt_of_weight_lt {σ : Type u_1} (m : MonomialOrder σ) (w : σ → ℕ) {a b : σ →₀ ℕ} (h : (Finsupp.weight w) a < (Finsupp.weight w) b) :
    (m.weightRefinement w).toSyn a < (m.weightRefinement w).toSyn b

    A strict weight comparison is a strict comparison in the refined order.

    source
    theorem MonomialOrder.weightRefinement_le_iff_of_weight_eq {σ : Type u_1} (m : MonomialOrder σ) (w : σ → ℕ) {a b : σ →₀ ℕ} (h : (Finsupp.weight w) a = (Finsupp.weight w) b) :
    (m.weightRefinement w).toSyn a ≤ (m.weightRefinement w).toSyn b ↔ m.toSyn a ≤ m.toSyn b

    Equal-weight monomials are compared by the original order.

    source
    theorem MonomialOrder.weightRefinement_lt_iff_of_weight_eq {σ : Type u_1} (m : MonomialOrder σ) (w : σ → ℕ) {a b : σ →₀ ℕ} (h : (Finsupp.weight w) a = (Finsupp.weight w) b) :
    (m.weightRefinement w).toSyn a < (m.weightRefinement w).toSyn b ↔ m.toSyn a < m.toSyn b

    Equal-weight monomials are strictly compared by the original order.

    source
    @[simp]
    theorem MonomialOrder.weightRefinement_zero_le_iff {σ : Type u_1} (m : MonomialOrder σ) {a b : σ →₀ ℕ} :
    (m.weightRefinement 0).toSyn a ≤ (m.weightRefinement 0).toSyn b ↔ m.toSyn a ≤ m.toSyn b

    Zero weight leaves all weak comparisons unchanged.

    source
    @[simp]
    theorem MonomialOrder.weightRefinement_zero_lt_iff {σ : Type u_1} (m : MonomialOrder σ) {a b : σ →₀ ℕ} :
    (m.weightRefinement 0).toSyn a < (m.weightRefinement 0).toSyn b ↔ m.toSyn a < m.toSyn b

    Zero weight leaves all strict comparisons unchanged.

    source
    theorem MonomialOrder.weightRefinement_single_le_iff {σ : Type u_1} (m : MonomialOrder σ) (w : σ → ℕ) {i j : σ} :
    (m.weightRefinement w).toSyn (Finsupp.single i 1) ≤ (m.weightRefinement w).toSyn (Finsupp.single j 1) ↔ w i < w j ∨ w i = w j ∧ m.toSyn (Finsupp.single i 1) ≤ m.toSyn (Finsupp.single j 1)

    The refined order compares variables by weight, retaining m to break ties.