Homogeneous lexicographic monomial ordering

• MonomialOrder.degLex: a variant of the lexicographic ordering that first compares degrees. 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 DegLex (σ →₀ ℕ) and the two lemmas MonomialOrder.degLex_le_iff and MonomialOrder.degLex_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

def DegLex (α : Type u_1) : Type u_1

A type synonym to equip a type with its lexicographic order sorted by degrees.

Equations

• DegLex α = α

@[match_pattern]

def toDegLex {α : Type u_1} : α ≃ DegLex α

toDegLex is the identity function to the DegLex of a type.

Equations

• toDegLex = Equiv.refl α

theorem toDegLex_injective {α : Type u_1} : Function.Injective ⇑toDegLex

theorem toDegLex_inj {α : Type u_1} {a b : α} : toDegLex a = toDegLex b ↔ a = b

@[match_pattern]

def ofDegLex {α : Type u_1} : DegLex α ≃ α

ofDegLex is the identity function from the DegLex of a type.

Equations

• ofDegLex = Equiv.refl (DegLex α)

theorem ofDegLex_injective {α : Type u_1} : Function.Injective ⇑ofDegLex

theorem ofDegLex_inj {α : Type u_1} {a b : DegLex α} : ofDegLex a = ofDegLex b ↔ a = b

@[simp]

theorem ofDegLex_symm_eq {α : Type u_1} : ofDegLex.symm = toDegLex

@[simp]

theorem toDegLex_symm_eq {α : Type u_1} : toDegLex.symm = ofDegLex

@[simp]

theorem ofDegLex_toDegLex {α : Type u_1} (a : α) : ofDegLex (toDegLex a) = a

@[simp]

theorem toDegLex_ofDegLex {α : Type u_1} (a : DegLex α) : toDegLex (ofDegLex a) = a

def DegLex.rec {α : Type u_1} {β : DegLex α → Sort u_2} (h : (a : α) → β (toDegLex a)) (a : DegLex α) : β a

A recursor for DegLex. Use as induction x.

Equations

• DegLex.rec h a = h (ofDegLex a)

@[simp]

theorem DegLex.forall_iff {α : Type u_1} {p : DegLex α → Prop} : (∀ (a : DegLex α), p a) ↔ ∀ (a : α), p (toDegLex a)

@[simp]

theorem DegLex.exists_iff {α : Type u_1} {p : DegLex α → Prop} : (∃ (a : DegLex α), p a) ↔ ∃ (a : α), p (toDegLex a)

noncomputable instance instAddCommMonoidDegLex {α : Type u_1} [AddCommMonoid α] : AddCommMonoid (DegLex α)

Equations

• instAddCommMonoidDegLex = ofDegLex.addCommMonoid

theorem toDegLex_add {α : Type u_1} [AddCommMonoid α] (a b : α) : toDegLex (a + b) = toDegLex a + toDegLex b

theorem ofDegLex_add {α : Type u_1} [AddCommMonoid α] (a b : DegLex α) : ofDegLex (a + b) = ofDegLex a + ofDegLex b

def Finsupp.DegLex {α : Type u_1} (r : α → α → Prop) (s : ℕ → ℕ → Prop) : (α →₀ ℕ) → (α →₀ ℕ) → Prop

Finsupp.DegLex r s is the homogeneous lexicographic order on α →₀ M, where α is ordered by r and M is ordered by s. The type synonym DegLex (α →₀ M) has an order given by Finsupp.DegLex (· < ·) (· < ·).

Equations

• Finsupp.DegLex r s = (Prod.Lex s (Finsupp.Lex r s) on fun (x : α →₀ ℕ) => (x.degree, x))

theorem Finsupp.degLex_def {α : Type u_1} {r : α → α → Prop} {s : ℕ → ℕ → Prop} {a b : α →₀ ℕ} : Finsupp.DegLex r s a b ↔ Prod.Lex s (Finsupp.Lex r s) (a.degree, a) (b.degree, b)

theorem Finsupp.DegLex.wellFounded {α : Type u_1} {r : α → α → Prop} [IsTrichotomous α r] (hr : WellFounded (Function.swap r)) {s : ℕ → ℕ → Prop} (hs : WellFounded s) (hs0 : ∀ ⦃n : ℕ⦄, ¬s n 0) : WellFounded (Finsupp.DegLex r s)

instance Finsupp.DegLex.instLTDegLexNat {α : Type u_1} [LT α] : LT (DegLex (α →₀ ℕ))

Equations

• Finsupp.DegLex.instLTDegLexNat = { lt := fun (f g : DegLex (α →₀ ℕ)) => Finsupp.DegLex (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : ℕ) => x1 < x2) (ofDegLex f) (ofDegLex g) }

theorem Finsupp.DegLex.lt_def {α : Type u_1} [LT α] {a b : DegLex (α →₀ ℕ)} : a < b ↔ toLex ((ofDegLex a).degree, toLex (ofDegLex a)) < toLex ((ofDegLex b).degree, toLex (ofDegLex b))

theorem Finsupp.DegLex.lt_iff {α : Type u_1} [LT α] {a b : DegLex (α →₀ ℕ)} : a < b ↔ (ofDegLex a).degree < (ofDegLex b).degree ∨ (ofDegLex a).degree = (ofDegLex b).degree ∧ toLex (ofDegLex a) < toLex (ofDegLex b)

instance Finsupp.DegLex.isStrictOrder {α : Type u_1} [LinearOrder α] : IsStrictOrder (DegLex (α →₀ ℕ)) fun (x1 x2 : DegLex (α →₀ ℕ)) => x1 < x2

instance Finsupp.DegLex.instLinearOrderDegLexNat {α : Type u_1} [LinearOrder α] : LinearOrder (DegLex (α →₀ ℕ))

The linear order on Finsupps obtained by the homogeneous lexicographic ordering.

Equations

• Finsupp.DegLex.instLinearOrderDegLexNat = LinearOrder.lift' (fun (f : DegLex (α →₀ ℕ)) => toLex ((ofDegLex f).degree, toLex (ofDegLex f))) ⋯

theorem Finsupp.DegLex.le_iff {α : Type u_1} [LinearOrder α] {x y : DegLex (α →₀ ℕ)} : x ≤ y ↔ (ofDegLex x).degree < (ofDegLex y).degree ∨ (ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y)

noncomputable instance Finsupp.DegLex.instOrderedCancelAddCommMonoidDegLexNat {α : Type u_1} [LinearOrder α] : OrderedCancelAddCommMonoid (DegLex (α →₀ ℕ))

Equations

• Finsupp.DegLex.instOrderedCancelAddCommMonoidDegLexNat = OrderedCancelAddCommMonoid.mk ⋯

noncomputable instance Finsupp.DegLex.instLinearOrderedCancelAddCommMonoidDegLexNat {α : Type u_1} [LinearOrder α] : LinearOrderedCancelAddCommMonoid (DegLex (α →₀ ℕ))

The linear order on Finsupps obtained by the homogeneous lexicographic ordering.

Equations

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

theorem Finsupp.DegLex.single_strictAnti {α : Type u_1} [LinearOrder α] : StrictAnti fun (a : α) => toDegLex (Finsupp.single a 1)

theorem Finsupp.DegLex.single_antitone {α : Type u_1} [LinearOrder α] : Antitone fun (a : α) => toDegLex (Finsupp.single a 1)

theorem Finsupp.DegLex.single_lt_iff {α : Type u_1} [LinearOrder α] {a b : α} : toDegLex (Finsupp.single b 1) < toDegLex (Finsupp.single a 1) ↔ a < b

theorem Finsupp.DegLex.single_le_iff {α : Type u_1} [LinearOrder α] {a b : α} : toDegLex (Finsupp.single b 1) ≤ toDegLex (Finsupp.single a 1) ↔ a ≤ b

theorem Finsupp.DegLex.monotone_degree {α : Type u_1} [LinearOrder α] : Monotone fun (x : DegLex (α →₀ ℕ)) => (ofDegLex x).degree

instance Finsupp.DegLex.orderBot {α : Type u_1} [LinearOrder α] : OrderBot (DegLex (α →₀ ℕ))

Equations

• Finsupp.DegLex.orderBot = OrderBot.mk ⋯

instance Finsupp.DegLex.wellFoundedLT {α : Type u_1} [LinearOrder α] [WellFoundedGT α] : WellFoundedLT (DegLex (α →₀ ℕ))

noncomputable def MonomialOrder.degLex {σ : Type u_2} [LinearOrder σ] [WellFoundedGT σ] : MonomialOrder σ

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

Equations

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

theorem MonomialOrder.degLex_le_iff {σ : Type u_2} [LinearOrder σ] [WellFoundedGT σ] {a b : σ →₀ ℕ} : MonomialOrder.degLex.toSyn a ≤ MonomialOrder.degLex.toSyn b ↔ toDegLex a ≤ toDegLex b

theorem MonomialOrder.degLex_lt_iff {σ : Type u_2} [LinearOrder σ] [WellFoundedGT σ] {a b : σ →₀ ℕ} : MonomialOrder.degLex.toSyn a < MonomialOrder.degLex.toSyn b ↔ toDegLex a < toDegLex b

theorem MonomialOrder.degLex_single_le_iff {σ : Type u_2} [LinearOrder σ] [WellFoundedGT σ] {a b : σ} : MonomialOrder.degLex.toSyn (Finsupp.single a 1) ≤ MonomialOrder.degLex.toSyn (Finsupp.single b 1) ↔ b ≤ a

theorem MonomialOrder.degLex_single_lt_iff {σ : Type u_2} [LinearOrder σ] [WellFoundedGT σ] {a b : σ} : MonomialOrder.degLex.toSyn (Finsupp.single a 1) < MonomialOrder.degLex.toSyn (Finsupp.single b 1) ↔ b < a