-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathGroebner.lean
206 lines (192 loc) · 7.33 KB
/
Groebner.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
import Mathlib.RingTheory.Polynomial.Basic
import Mathlib.RingTheory.MvPolynomial.Ideal
import Mathlib.RingTheory.Ideal.Basic
import Mathlib.Data.Set.Finite
import Mathlib.Tactic.LibrarySearch
import Mathlib.Data.Finsupp.Pwo
import Mathlib.RingTheory.Finiteness
import Multideg
import Ideal
import Division
import Set
open Classical
open BigOperators
open Ideal
namespace MvPolynomial
variable {σ : Type _} {s : σ →₀ ℕ} {k : Type _} [Field k]
variable [term_order_class: TermOrderClass (TermOrder (σ→₀ℕ))]
variable (p : MvPolynomial σ k)
variable (G': Finset (MvPolynomial σ k)) (I : Ideal (MvPolynomial σ k))
set_option synthInstance.maxHeartbeats 40000
def is_groebner_basis :=
G'.toSet ⊆ I ∧ leading_term_ideal I = leading_term_ideal G'.toSet
theorem exists_groebner_basis [Finite σ] :
∃ G' : Finset (MvPolynomial σ k), is_groebner_basis G' I := by
let ltideal : Ideal (MvPolynomial σ k) := leading_term_ideal I
have key : Ideal.FG ltideal := (inferInstance : IsNoetherian _ _).noetherian _
simp only [leading_term_ideal] at key
rw [Ideal.fg_span_iff_fg_span_finset_subset] at key
rcases key with ⟨s, hs, h⟩
have := Set.subset_image hs
have ⟨G', hG', h'⟩ := Set.finset_subset_preimage_of_finite_image
(this.symm ▸ Finset.finite_toSet s)
use G'
constructor
·exact (Set.subset_inter_iff.mp hG').1
· rw [this] at h'
unfold leading_term_ideal
rw [h', h]
lemma groebner_basis_self {G' : Finset (MvPolynomial σ k)}
{I : Ideal (MvPolynomial σ k)} (h : is_groebner_basis G' I) :
is_groebner_basis G' (span G') := by
constructor
·
exact subset_span
·
rw [←SetLike.coe_set_eq]
apply Set.eq_of_subset_of_subset
·
rw [←h.2, leading_term_ideal, leading_term_ideal]
apply Ideal.span_mono
apply Set.image_subset
rw [SetLike.coe_subset_coe, span_le]
exact h.1
·
rw [leading_term_ideal, leading_term_ideal]
apply Ideal.span_mono
apply Set.image_subset
exact subset_span
theorem groebner_basis_rem_eq_zero_iff {p : MvPolynomial σ k}
{G' : Finset (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)}
{r : MvPolynomial σ k}
(h : is_groebner_basis G' I) (hG' : is_rem p G' r):
r = 0 ↔ p ∈ I := by
constructor
· intro hr
rw [hr] at hG'
exact (rem_mem_ideal_iff h.1 hG').mp I.zero_mem
· intro hp
by_contra hr
apply rem_term_not_mem_leading_term_ideal hG' r.multideg
· rw [mem_support_iff, ←leading_coeff_def]
exact r.leading_coeff_eq_zero_iff.not.mpr hr
rw [←leading_coeff_def, ←leading_term_def, ←h.2, leading_term_ideal]
apply Set.mem_of_subset_of_mem subset_span
exact Set.mem_image_of_mem
leading_term ((rem_mem_ideal_iff h.1 hG').mpr hp)
theorem groebner_basis_rem_eq_zero_iff' {p : MvPolynomial σ k}
{G' : Finset (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)}
(h : is_groebner_basis G' I) : is_rem p G' 0 ↔ p ∈ I := by
constructor
· intro hp
exact (groebner_basis_rem_eq_zero_iff h hp).mp rfl
· intro hp
have :=
(groebner_basis_rem_eq_zero_iff h (exists_rem p G').choose_spec).mpr hp
exact this ▸ (exists_rem p G').choose_spec
theorem groebner_basis_def :
is_groebner_basis G' I ↔ G'.toSet ⊆ I ∧ ∀ p ∈ I, is_rem p G' 0 := by
constructor
· intro h
constructor
·exact h.1
· intro p hp
exact (groebner_basis_rem_eq_zero_iff' h).mpr hp
· rintro ⟨hG', hp⟩
constructor
·exact hG'
·
have hG' : I = span G' := by
rw [←SetLike.coe_set_eq]
refine Set.eq_of_subset_of_subset ?_ (span_le.mpr hG')
intro p hp'
rw [SetLike.mem_coe, ←rem_mem_ideal_iff subset_span (hp p hp')]
exact Ideal.zero_mem _
rw [hG', ←SetLike.coe_set_eq]
apply Set.eq_of_subset_of_subset
· apply span_le.mpr
intro p'
intro hp'
rcases hp' with ⟨p,hp', hp'₁⟩
rw [←hp'₁]
specialize hp p (hG'.symm ▸ hp')
rcases hp with ⟨_, q, hrq, hp⟩
rw [add_zero] at hp
simp [leading_term_ideal_span_monomial, mem_ideal_span_monomial_image,
leading_term_def]
intro h
rw [←(leading_coeff_eq_zero_iff _).not, leading_coeff_def] at h
nth_rewrite 2 [hp] at h
rw [Finsupp.sum, coeff_sum] at h
obtain ⟨⟨g, hg⟩, hg₁⟩ :
∃ (g : { x // x ∈ G' }), (g * q g).coeff p.multideg ≠ 0 := by
by_contra' hg
simp [hg] at h
use g
rw [←mem_support_iff] at hg₁
have gqg_ne_0 : g * q ⟨g, hg⟩ ≠ 0 := by
apply support_eq_empty.not.mp
exact Finset.nonempty_iff_ne_empty.mp (Set.nonempty_of_mem hg₁)
have ⟨g_ne_0, qg_ne_0⟩ := ne_zero_and_ne_zero_of_mul gqg_ne_0
constructor
·exact ⟨hg, g_ne_0⟩
· specialize hrq g hg
have hrq := multideg_le_multideg_of_multideg''_le_multideg'' hrq
have hg₂ := le_multideg hg₁
rw [←eq_of_le_of_not_lt hrq (not_lt_of_le hg₂)]
rw [←multideg'_eq_multideg gqg_ne_0]
rw [multideg'_mul g_ne_0 qg_ne_0]
rw [multideg'_eq_multideg]
rw [le_add_iff_nonneg_right]
exact zero_le _
· unfold leading_term_ideal
apply span_le.mpr
refine subset_trans ?_ subset_span
exact Set.image_subset _ subset_span
theorem groebner_basis_is_basis
{G': Finset (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)}
(h : is_groebner_basis G' I) : I = span G' := by
rw [←SetLike.coe_set_eq]
apply Set.eq_of_subset_of_subset
· intro p hp
simp
have hr := (exists_rem p G').choose_spec
have := (groebner_basis_rem_eq_zero_iff h hr).mpr hp
let q := hr.2.choose
have hq := hr.2.choose_spec.2
have hrem : (exists_rem p G').choose = p - q.sum (·*·) := by
conv => enter [2] ; rw [hq]
ring
rw [hrem] at this
have := eq_of_sub_eq_zero this
rw [this]
exact sum_mul_mem_of_subset' subset_span q
·simp [span_le, h.1]
theorem groebner_basis_unique_rem
{G': Finset (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)}
(h : is_groebner_basis G' I) :
∃! (r : MvPolynomial σ k), is_rem p G' r := by
apply exists_unique_of_exists_of_unique (exists_rem p G')
intros r₁ r₂ hr₁ hr₂
by_contra' hr
have hr := sub_ne_zero_of_ne hr
have : (r₁-r₂).multideg ∈ (r₁-r₂).support := by
simp [hr, ←(multideg'_eq_multideg hr), multideg']
exact Finset.max'_mem _ _
apply rem_sub_rem_term_not_mem_leading_term_ideal hr₁ hr₂ (r₁-r₂).multideg this
rw [←h.2, leading_term_ideal, ←leading_coeff_def, ←leading_term_def]
have := Set.mem_image_of_mem leading_term (rem_sub_rem_mem_ideal h.1 hr₁ hr₂)
exact Set.mem_of_subset_of_mem subset_span this
-- noncomputable def groebner_rem
-- {G': Finset (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)}
-- (h : is_groebner_basis G' I) :=
-- (p.groebner_basis_unique_rem h).choose
-- lemma groebner_rem_eq
-- {G': Finset (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)}
-- (h : is_groebner_basis G' I) :
-- p.groebner_rem h = p.rem G'.toList := by sorry
-- theorem mem_ideal_iff_groebner_rem_eq_zero
-- {G': Finset (MvPolynomial σ k)} {I : Ideal (MvPolynomial σ k)}
-- (h : is_groebner_basis G' I) :
-- p ∈ I ↔ p.groebner_rem h = 0 := by sorry
-- #check 1