Monomial orders

Monomial orders

A monomial order is well ordering relation on a type of the form σ →₀ ℕ which is compatible with addition and for which 0 is the smallest element. Since several monomial orders may have to be used simultaneously, one cannot get them as instances.

In this formalization, they are presented as a structure MonomialOrder which encapsulates MonomialOrder.toSyn, an additive and monotone isomorphism to a linearly ordered cancellative additive commutative monoid. The entry MonomialOrder.wf asserts that MonomialOrder.syn is well founded.

The terminology comes from commutative algebra and algebraic geometry, especially Gröbner bases, where c : σ →₀ ℕ are exponents of monomials.

Given a monomial order m : MonomialOrder σ, we provide the notation c ≼[m] d and c ≺[m] d to compare c d : σ →₀ ℕ with respect to m. It is activated using open scoped MonomialOrder.

Examples

Commutative algebra defines many monomial orders, with different usefulness ranges. In this file, we provide the basic example of lexicographic ordering. For the graded lexicographic ordering, see Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean

• MonomialOrder.lex : the lexicographic ordering on σ →₀ ℕ. For this, σ needs to be embedded with an ordering relation which satisfies WellFoundedGT σ. (This last property is automatic when σ is finite).

The type synonym is Lex (σ →₀ ℕ) and the two lemmas MonomialOrder.lex_le_iff and MonomialOrder.lex_lt_iff rewrite the ordering as comparisons in the type Lex (σ →₀ ℕ).

References

• [Cox, Little and O'Shea, Ideals, varieties, and algorithms][coxlittleoshea1997]
• [Becker and Weispfenning, Gröbner bases][Becker-Weispfenning1993]

Note

In algebraic geometry, when the finitely many variables are indexed by integers, it is customary to order them using the opposite order : MvPolynomial.X 0 > MvPolynomial.X 1 > …

structure MonomialOrder (σ : Type u_1) : Type (max u_1 (u_2 + 1))

Monomial orders : equivalence of σ →₀ ℕ with a well-ordered type

• syn : Type u_2

  The synonym type

• addCommMonoidSyn : AddCommMonoid self.syn

  syn is an additive commutative monoid

• linearOrderSyn : LinearOrder self.syn

  syn is linearly ordered

• isOrderedAddMonoid_syn : IsOrderedAddMonoid self.syn

  syn is a linearly ordered cancellative additive commutative monoid

• toSyn : (σ →₀ ℕ) ≃+ self.syn

  the additive equivalence from σ →₀ ℕ to syn

• toSyn_monotone : Monotone ⇑self.toSyn

  toSyn is monotone

• wellFoundedLT_syn : WellFoundedLT self.syn

  syn is a well ordering

@[deprecated MonomialOrder.addCommMonoidSyn (since := "2026-07-07")]

def acm {σ : Type u_1} (self : MonomialOrder σ) : AddCommMonoid self.syn

Alias of MonomialOrder.addCommMonoidSyn.

---

syn is an additive commutative monoid

Equations

• @acm = @MonomialOrder.addCommMonoidSyn

@[deprecated MonomialOrder.linearOrderSyn (since := "2026-07-07")]

def lo {σ : Type u_1} (self : MonomialOrder σ) : LinearOrder self.syn

Alias of MonomialOrder.linearOrderSyn.

---

syn is linearly ordered

Equations

• @lo = @MonomialOrder.linearOrderSyn

@[deprecated MonomialOrder.wellFoundedLT_syn (since := "2026-07-07")]

theorem wf {σ : Type u_1} (self : MonomialOrder σ) : WellFoundedLT self.syn

Alias of MonomialOrder.wellFoundedLT_syn.

---

syn is a well ordering

@[implicit_reducible]

instance MonomialOrder.instAddCancelCommMonoidSyn {σ : Type u_1} (m : MonomialOrder σ) : AddCancelCommMonoid m.syn

Equations

• m.instAddCancelCommMonoidSyn = { toAddCommMonoid := m.addCommMonoidSyn, toIsLeftCancelAdd := ⋯ }

instance MonomialOrder.isOrderedCancelAddMonoid_syn {σ : Type u_1} (m : MonomialOrder σ) : IsOrderedCancelAddMonoid m.syn

@[deprecated MonomialOrder.isOrderedCancelAddMonoid_syn (since := "2026-07-07")]

theorem MonomialOrder.iocam {σ : Type u_1} (m : MonomialOrder σ) : IsOrderedCancelAddMonoid m.syn

Alias of MonomialOrder.isOrderedCancelAddMonoid_syn.

theorem MonomialOrder.le_add_right {σ : Type u_1} (m : MonomialOrder σ) (a b : σ →₀ ℕ) : m.toSyn a ≤ m.toSyn a + m.toSyn b

@[implicit_reducible]

instance MonomialOrder.orderBot {σ : Type u_1} (m : MonomialOrder σ) : OrderBot m.syn

Equations

• m.orderBot = { bot := 0, bot_le := ⋯ }

@[simp]

theorem MonomialOrder.bot_eq_zero {σ : Type u_1} (m : MonomialOrder σ) : ⊥ = 0

@[simp]

theorem MonomialOrder.zero_le {σ : Type u_1} (m : MonomialOrder σ) (a : m.syn) : 0 ≤ a

theorem MonomialOrder.eq_zero_iff {σ : Type u_1} (m : MonomialOrder σ) {a : m.syn} : a = 0 ↔ a ≤ 0

theorem MonomialOrder.toSyn_eq_zero_iff {σ : Type u_1} (m : MonomialOrder σ) (a : σ →₀ ℕ) : m.toSyn a = 0 ↔ a = 0

theorem MonomialOrder.toSyn_lt_iff_ne_zero {σ : Type u_1} (m : MonomialOrder σ) {a : m.syn} : 0 < a ↔ a ≠ 0

theorem MonomialOrder.toSyn_strictMono {σ : Type u_1} (m : MonomialOrder σ) : StrictMono ⇑m.toSyn

def MonomialOrder.«term_≺[_]_» : Lean.TrailingParserDescr

Given a monomial order, notation for the corresponding strict order relation on σ →₀ ℕ

Equations

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

def MonomialOrder.«term_≼[_]_» : Lean.TrailingParserDescr

Given a monomial order, notation for the corresponding order relation on σ →₀ ℕ

Equations

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

instance instIsOrderedCancelAddMonoidLexFinsupp {α : Type u_1} {N : Type u_2} [LinearOrder α] [AddCommMonoid N] [PartialOrder N] [IsOrderedCancelAddMonoid N] : IsOrderedCancelAddMonoid (Lex (α →₀ N))

noncomputable def MonomialOrder.lex {σ : Type u_1} [LinearOrder σ] [WellFoundedGT σ] : MonomialOrder σ

The lexicographic order on σ →₀ ℕ, as a MonomialOrder

Equations

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

theorem MonomialOrder.lex_le_iff {σ : Type u_1} [LinearOrder σ] [WellFoundedGT σ] {c d : σ →₀ ℕ} : lex.toSyn c ≤ lex.toSyn d ↔ toLex c ≤ toLex d

theorem MonomialOrder.lex_lt_iff {σ : Type u_1} [LinearOrder σ] [WellFoundedGT σ] {c d : σ →₀ ℕ} : lex.toSyn c < lex.toSyn d ↔ toLex c < toLex d

theorem MonomialOrder.lex_lt_iff_of_unique {σ : Type u_1} [LinearOrder σ] [Unique σ] {c d : σ →₀ ℕ} : lex.toSyn c < lex.toSyn d ↔ c default < d default

theorem MonomialOrder.lex_le_iff_of_unique {σ : Type u_1} [LinearOrder σ] [Unique σ] {c d : σ →₀ ℕ} : lex.toSyn c ≤ lex.toSyn d ↔ c default ≤ d default