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/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
• Becker and Weispfenning, Gröbner bases

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

• locacm : LinearOrderedCancelAddCommMonoid 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

• wf : WellFoundedLT self.syn

  syn is a well ordering

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

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

Equations

• m.orderBot = OrderBot.mk ⋯

@[simp]

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

theorem MonomialOrder.eq_zero_iff {σ : Type u_1} (m : MonomialOrder σ) {a : m.syn} : a = 0 ↔ 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.

noncomputable instance instOrderedCancelAddCommMonoidLexFinsuppOfLinearOrder {α : Type u_1} {N : Type u_2} [LinearOrder α] [OrderedCancelAddCommMonoid N] : OrderedCancelAddCommMonoid (Lex (α →₀ N))

Equations

• instOrderedCancelAddCommMonoidLexFinsuppOfLinearOrder = OrderedCancelAddCommMonoid.mk ⋯

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

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

Equations

• MonomialOrder.lex = { syn := Lex (σ →₀ ℕ), locacm := inferInstance, toSyn := { toEquiv := toLex, map_add' := ⋯ }, toSyn_monotone := ⋯, wf := ⋯ }

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