Skip to content

Commit 0257491

Browse files
AntoineChambert-LoirAntoineChambert-Loir
committed
feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order (#19455)
Definition of the homogeneous lexicographic order This is part of an ongoing work on basic of Gröbner theory. A subsequent PR will add the homogeneous reverse lexicographic order.
1 parent 0e2973b commit 0257491

File tree

4 files changed

+293
-0
lines changed

4 files changed

+293
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2483,6 +2483,7 @@ import Mathlib.Data.Finsupp.Indicator
24832483
import Mathlib.Data.Finsupp.Interval
24842484
import Mathlib.Data.Finsupp.Lex
24852485
import Mathlib.Data.Finsupp.MonomialOrder
2486+
import Mathlib.Data.Finsupp.MonomialOrder.DegLex
24862487
import Mathlib.Data.Finsupp.Multiset
24872488
import Mathlib.Data.Finsupp.NeLocus
24882489
import Mathlib.Data.Finsupp.Notation

‎Mathlib/Data/Finsupp/Lex.lean‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,26 @@ instance Lex.linearOrder [LinearOrder N] : LinearOrder (Lex (α →₀ N)) where
7575
le := (· ≤ ·)
7676
__ := LinearOrder.lift' (toLex ∘ toDFinsupp ∘ ofLex) finsuppEquivDFinsupp.injective
7777

78+
theorem Lex.single_strictAnti : StrictAnti (fun (a : α) ↦ toLex (single a 1)) := by
79+
intro a b h
80+
simp only [LT.lt, Finsupp.lex_def]
81+
simp only [ofLex_toLex, Nat.lt_eq]
82+
use a
83+
constructor
84+
· intro d hd
85+
simp only [Finsupp.single_eq_of_ne (ne_of_lt hd).symm,
86+
Finsupp.single_eq_of_ne (ne_of_gt (lt_trans hd h))]
87+
· simp only [single_eq_same, single_eq_of_ne (ne_of_lt h).symm, zero_lt_one]
88+
89+
theorem Lex.single_lt_iff {a b : α} : toLex (single b 1) < toLex (single a 1) ↔ a < b :=
90+
Lex.single_strictAnti.lt_iff_lt
91+
92+
theorem Lex.single_le_iff {a b : α} : toLex (single b 1) ≤ toLex (single a 1) ↔ a ≤ b :=
93+
Lex.single_strictAnti.le_iff_le
94+
95+
theorem Lex.single_antitone : Antitone (fun (a : α) ↦ toLex (single a 1)) :=
96+
Lex.single_strictAnti.antitone
97+
7898
variable [PartialOrder N]
7999

80100
theorem toLex_monotone : Monotone (@toLex (α →₀ N)) :=

‎Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean‎

Lines changed: 258 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,258 @@
1+
/-
2+
Copyright (c) 2024 Antoine Chambert-Loir. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Antoine Chambert-Loir
5+
-/
6+
7+
import Mathlib.Data.Finsupp.MonomialOrder
8+
import Mathlib.Data.Finsupp.Weight
9+
import Mathlib.Logic.Equiv.TransferInstance
10+
11+
/-! Homogeneous lexicographic monomial ordering
12+
13+
* `MonomialOrder.degLex`: a variant of the lexicographic ordering that first compares degrees.
14+
For this, `σ` needs to be embedded with an ordering relation which satisfies `WellFoundedGT σ`.
15+
(This last property is automatic when `σ` is finite).
16+
17+
The type synonym is `DegLex (σ →₀ ℕ)` and the two lemmas `MonomialOrder.degLex_le_iff`
18+
and `MonomialOrder.degLex_lt_iff` rewrite the ordering as comparisons in the type `Lex (σ →₀ ℕ)`.
19+
20+
## References
21+
22+
* [Cox, Little and O'Shea, *Ideals, varieties, and algorithms*][coxlittleoshea1997]
23+
* [Becker and Weispfenning, *Gröbner bases*][Becker-Weispfenning1993]
24+
25+
-/
26+
27+
section degLex
28+
29+
/-- A type synonym to equip a type with its lexicographic order sorted by degrees. -/
30+
def DegLex (α : Type*) := α
31+
32+
variable {α : Type*}
33+
34+
/-- `toDegLex` is the identity function to the `DegLex` of a type. -/
35+
@[match_pattern] def toDegLex : α ≃ DegLex α := Equiv.refl _
36+
37+
theorem toDegLex_injective : Function.Injective (toDegLex (α := α)) := fun _ _ ↦ _root_.id
38+
39+
theorem toDegLex_inj {a b : α} : toDegLex a = toDegLex b ↔ a = b := Iff.rfl
40+
41+
/-- `ofDegLex` is the identity function from the `DegLex` of a type. -/
42+
@[match_pattern] def ofDegLex : DegLex α ≃ α := Equiv.refl _
43+
44+
theorem ofDegLex_injective : Function.Injective (ofDegLex (α := α)) := fun _ _ ↦ _root_.id
45+
46+
theorem ofDegLex_inj {a b : DegLex α} : ofDegLex a = ofDegLex b ↔ a = b := Iff.rfl
47+
48+
@[simp] theorem ofDegLex_symm_eq : (@ofDegLex α).symm = toDegLex := rfl
49+
50+
@[simp] theorem toDegLex_symm_eq : (@toDegLex α).symm = ofDegLex := rfl
51+
52+
@[simp] theorem ofDegLex_toDegLex (a : α) : ofDegLex (toDegLex a) = a := rfl
53+
54+
@[simp] theorem toDegLex_ofDegLex (a : DegLex α) : toDegLex (ofDegLex a) = a := rfl
55+
56+
/-- A recursor for `DegLex`. Use as `induction x`. -/
57+
@[elab_as_elim, induction_eliminator, cases_eliminator]
58+
protected def DegLex.rec {β : DegLex α → Sort*} (h : ∀ a, β (toDegLex a)) :
59+
∀ a, β a := fun a => h (ofDegLex a)
60+
61+
@[simp] lemma DegLex.forall_iff {p : DegLex α → Prop} : (∀ a, p a) ↔ ∀ a, p (toDegLex a) := Iff.rfl
62+
@[simp] lemma DegLex.exists_iff {p : DegLex α → Prop} : (∃ a, p a) ↔ ∃ a, p (toDegLex a) := Iff.rfl
63+
64+
noncomputable instance [AddCommMonoid α] :
65+
AddCommMonoid (DegLex α) := ofDegLex.addCommMonoid
66+
67+
theorem toDegLex_add [AddCommMonoid α] (a b : α) :
68+
toDegLex (a + b) = toDegLex a + toDegLex b := rfl
69+
70+
theorem ofDegLex_add [AddCommMonoid α] (a b : DegLex α) :
71+
ofDegLex (a + b) = ofDegLex a + ofDegLex b := rfl
72+
73+
namespace Finsupp
74+
75+
/-- `Finsupp.DegLex r s` is the homogeneous lexicographic order on `α →₀ M`,
76+
where `α` is ordered by `r` and `M` is ordered by `s`.
77+
The type synonym `DegLex (α →₀ M)` has an order given by `Finsupp.DegLex (· < ·) (· < ·)`. -/
78+
protected def DegLex (r : α → α → Prop) (s : ℕ → ℕ → Prop) :
79+
(α →₀ ℕ) → (α →₀ ℕ) → Prop :=
80+
(Prod.Lex s (Finsupp.Lex r s)) on (fun x ↦ (x.degree, x))
81+
82+
theorem degLex_def {r : α → α → Prop} {s : ℕ → ℕ → Prop} {a b : α →₀ ℕ} :
83+
Finsupp.DegLex r s a b ↔ Prod.Lex s (Finsupp.Lex r s) (a.degree, a) (b.degree, b) :=
84+
Iff.rfl
85+
86+
namespace DegLex
87+
88+
theorem wellFounded
89+
{r : α → α → Prop} [IsTrichotomous α r] (hr : WellFounded (Function.swap r))
90+
{s : ℕ → ℕ → Prop} (hs : WellFounded s) (hs0 : ∀ ⦃n⦄, ¬ s n 0) :
91+
WellFounded (Finsupp.DegLex r s) := by
92+
have wft := WellFounded.prod_lex hs (Finsupp.Lex.wellFounded' hs0 hs hr)
93+
rw [← Set.wellFoundedOn_univ] at wft
94+
unfold Finsupp.DegLex
95+
rw [← Set.wellFoundedOn_range]
96+
exact Set.WellFoundedOn.mono wft (le_refl _) (fun _ _ ↦ trivial)
97+
98+
instance [LT α] : LT (DegLex (α →₀ ℕ)) :=
99+
⟨fun f g ↦ Finsupp.DegLex (· < ·) (· < ·) (ofDegLex f) (ofDegLex g)⟩
100+
101+
theorem lt_def [LT α] {a b : DegLex (α →₀ ℕ)} :
102+
a < b ↔ (toLex ((ofDegLex a).degree, toLex (ofDegLex a))) <
103+
(toLex ((ofDegLex b).degree, toLex (ofDegLex b))) :=
104+
Iff.rfl
105+
106+
theorem lt_iff [LT α] {a b : DegLex (α →₀ ℕ)} :
107+
a < b ↔ (ofDegLex a).degree < (ofDegLex b).degree ∨
108+
(((ofDegLex a).degree = (ofDegLex b).degree) ∧ toLex (ofDegLex a) < toLex (ofDegLex b)) := by
109+
simp only [lt_def, Prod.Lex.lt_iff]
110+
111+
variable [LinearOrder α]
112+
113+
instance isStrictOrder : IsStrictOrder (DegLex (α →₀ ℕ)) (· < ·) where
114+
irrefl := fun a ↦ by simp [lt_def]
115+
trans := by
116+
intro a b c hab hbc
117+
simp only [lt_iff] at hab hbc ⊢
118+
rcases hab with (hab | hab)
119+
· rcases hbc with (hbc | hbc)
120+
· left; exact lt_trans hab hbc
121+
· left; exact lt_of_lt_of_eq hab hbc.1
122+
· rcases hbc with (hbc | hbc)
123+
· left; exact lt_of_eq_of_lt hab.1 hbc
124+
· right; exact ⟨Eq.trans hab.1 hbc.1, lt_trans hab.2 hbc.2⟩
125+
126+
/-- The linear order on `Finsupp`s obtained by the homogeneous lexicographic ordering. -/
127+
instance : LinearOrder (DegLex (α →₀ ℕ)) :=
128+
LinearOrder.lift'
129+
(fun (f : DegLex (α →₀ ℕ)) ↦ toLex ((ofDegLex f).degree, toLex (ofDegLex f)))
130+
(fun f g ↦ by simp)
131+
132+
theorem le_iff {x y : DegLex (α →₀ ℕ)} :
133+
x ≤ y ↔ (ofDegLex x).degree < (ofDegLex y).degree ∨
134+
(ofDegLex x).degree = (ofDegLex y).degree ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y) := by
135+
simp only [le_iff_eq_or_lt, lt_iff, EmbeddingLike.apply_eq_iff_eq]
136+
by_cases h : x = y
137+
· simp [h]
138+
· by_cases k : (ofDegLex x).degree < (ofDegLex y).degree
139+
· simp [k]
140+
· simp only [h, k, false_or]
141+
142+
noncomputable instance : OrderedCancelAddCommMonoid (DegLex (α →₀ ℕ)) where
143+
le_of_add_le_add_left a b c h := by
144+
rw [le_iff] at h ⊢
145+
simpa only [ofDegLex_add, degree_add, add_lt_add_iff_left, add_right_inj, toLex_add,
146+
add_le_add_iff_left] using h
147+
add_le_add_left a b h c := by
148+
rw [le_iff] at h ⊢
149+
simpa [ofDegLex_add, degree_add] using h
150+
151+
/-- The linear order on `Finsupp`s obtained by the homogeneous lexicographic ordering. -/
152+
noncomputable instance :
153+
LinearOrderedCancelAddCommMonoid (DegLex (α →₀ ℕ)) where
154+
le_total := instLinearOrderDegLexNat.le_total
155+
decidableLE := instLinearOrderDegLexNat.decidableLE
156+
compare_eq_compareOfLessAndEq := instLinearOrderDegLexNat.compare_eq_compareOfLessAndEq
157+
158+
theorem single_strictAnti : StrictAnti (fun (a : α) ↦ toDegLex (single a 1)) := by
159+
intro _ _ h
160+
simp only [lt_iff, ofDegLex_toDegLex, degree_single, lt_self_iff_false, Lex.single_lt_iff, h,
161+
and_self, or_true]
162+
163+
theorem single_antitone : Antitone (fun (a : α) ↦ toDegLex (single a 1)) :=
164+
single_strictAnti.antitone
165+
166+
theorem single_lt_iff {a b : α} :
167+
toDegLex (Finsupp.single b 1) < toDegLex (Finsupp.single a 1) ↔ a < b :=
168+
single_strictAnti.lt_iff_lt
169+
170+
theorem single_le_iff {a b : α} :
171+
toDegLex (Finsupp.single b 1) ≤ toDegLex (Finsupp.single a 1) ↔ a ≤ b :=
172+
single_strictAnti.le_iff_le
173+
174+
theorem monotone_degree :
175+
Monotone (fun (x : DegLex (α →₀ ℕ)) ↦ (ofDegLex x).degree) := by
176+
intro x y
177+
rw [le_iff]
178+
rintro (h | h)
179+
· apply le_of_lt h
180+
· apply le_of_eq h.1
181+
182+
instance orderBot : OrderBot (DegLex (α →₀ ℕ)) where
183+
bot := toDegLex (0 : α →₀ ℕ)
184+
bot_le x := by
185+
simp only [le_iff, ofDegLex_toDegLex, toLex_zero, degree_zero]
186+
rcases eq_zero_or_pos (ofDegLex x).degree with (h | h)
187+
· simp only [h, lt_self_iff_false, true_and, false_or, ge_iff_le]
188+
exact bot_le
189+
· simp [h]
190+
191+
instance wellFoundedLT [WellFoundedGT α] :
192+
WellFoundedLT (DegLex (α →₀ ℕ)) :=
193+
⟨wellFounded wellFounded_gt wellFounded_lt fun n ↦ (zero_le n).not_lt⟩
194+
195+
end DegLex
196+
197+
end Finsupp
198+
199+
namespace MonomialOrder
200+
201+
open Finsupp
202+
203+
variable {σ : Type*} [LinearOrder σ] [WellFoundedGT σ]
204+
205+
/-- The deg-lexicographic order on `σ →₀ ℕ`, as a `MonomialOrder` -/
206+
noncomputable def degLex :
207+
MonomialOrder σ where
208+
syn := DegLex (σ →₀ ℕ)
209+
toSyn := { toEquiv := toDegLex, map_add' := toDegLex_add }
210+
toSyn_monotone a b h := by
211+
simp only [AddEquiv.coe_mk, DegLex.le_iff, ofDegLex_toDegLex]
212+
by_cases ha : a.degree < b.degree
213+
· exact Or.inl ha
214+
· refine Or.inr ⟨le_antisymm ?_ (not_lt.mp ha), toLex_monotone h⟩
215+
rw [← add_tsub_cancel_of_le h, degree_add]
216+
exact Nat.le_add_right a.degree (b - a).degree
217+
218+
theorem degLex_le_iff {a b : σ →₀ ℕ} :
219+
a ≼[degLex] b ↔ toDegLex a ≤ toDegLex b :=
220+
Iff.rfl
221+
222+
theorem degLex_lt_iff {a b : σ →₀ ℕ} :
223+
a ≺[degLex] b ↔ toDegLex a < toDegLex b :=
224+
Iff.rfl
225+
226+
theorem degLex_single_le_iff {a b : σ} :
227+
single a 1 ≼[degLex] single b 1 ↔ b ≤ a := by
228+
rw [MonomialOrder.degLex_le_iff, DegLex.single_le_iff]
229+
230+
theorem degLex_single_lt_iff {a b : σ} :
231+
single a 1 ≺[degLex] single b 1 ↔ b < a := by
232+
rw [MonomialOrder.degLex_lt_iff, DegLex.single_lt_iff]
233+
234+
end MonomialOrder
235+
236+
section Examples
237+
238+
open Finsupp MonomialOrder DegLex
239+
240+
/-- for the deg-lexicographic ordering, X 1 < X 0 -/
241+
example : single (1 : Fin 2) 1 ≺[degLex] single 0 1 := by
242+
rw [degLex_lt_iff, single_lt_iff]
243+
exact Nat.one_pos
244+
245+
/-- for the deg-lexicographic ordering, X 0 * X 1 < X 0 ^ 2 -/
246+
example : (single 0 1 + single 1 1) ≺[degLex] single (0 : Fin 2) 2 := by
247+
simp only [degLex_lt_iff, lt_iff, ofDegLex_toDegLex, degree_add,
248+
degree_single, Nat.reduceAdd, lt_self_iff_false, true_and, false_or]
249+
use 0
250+
simp
251+
252+
/-- for the deg-lexicographic ordering, X 0 < X 1 ^ 2 -/
253+
example : single (0 : Fin 2) 1 ≺[degLex] single 1 2 := by
254+
simp [degLex_lt_iff, lt_iff]
255+
256+
end Examples
257+
258+
end degLex

‎Mathlib/Data/Finsupp/Weight.lean‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,20 @@ def degree (d : σ →₀ ℕ) := ∑ i ∈ d.support, d i
202202
@[deprecated degree (since := "2024-07-20")]
203203
alias _root_.MvPolynomial.degree := degree
204204

205+
@[simp]
206+
theorem degree_add (a b : σ →₀ ℕ) : (a + b).degree = a.degree + b.degree :=
207+
sum_add_index' (h := fun _ ↦ id) (congrFun rfl) fun _ _ ↦ congrFun rfl
208+
209+
@[simp]
210+
theorem degree_single (a : σ) (m : ℕ) : (Finsupp.single a m).degree = m := by
211+
rw [degree, Finset.sum_eq_single a]
212+
· simp only [single_eq_same]
213+
· intro b _ hba
214+
exact single_eq_of_ne hba.symm
215+
· intro ha
216+
simp only [mem_support_iff, single_eq_same, ne_eq, Decidable.not_not] at ha
217+
rw [single_eq_same, ha]
218+
205219
lemma degree_eq_zero_iff (d : σ →₀ ℕ) : degree d = 0 ↔ d = 0 := by
206220
simp only [degree, Finset.sum_eq_zero_iff, Finsupp.mem_support_iff, ne_eq, Decidable.not_imp_self,
207221
DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply]

0 commit comments

Comments
 (0)