Weak Division

Reference

• "On the construction of Gröbner bases using syzygies" https://www.sciencedirect.com/science/article/pii/S074771718880052X

instance Pi.irrefl_lex {ι : Type u_3} {β : ι → Type u_4} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) [∀ (i : ι), Std.Irrefl s] : Std.Irrefl (Pi.Lex r s)

theorem Finset.apply_piecewise_congr {α : Type u_4} {π : α → Type u_3} {f g : (i : α) → π i} (s t : Finset α) (a : α) [(a : α) → Decidable (a ∈ s)] [(a : α) → Decidable (a ∈ t)] (ha : a ∈ s ↔ a ∈ t) : s.piecewise f g a = t.piecewise f g a

theorem Finset.Colex.lt_iff {α : Type u_3} [LinearOrder α] (l₁ l₂ : Colex (Finset α)) : l₁ < l₂ ↔ ∃ (a : α), (∀ b > a, b ∈ ofColex l₁ ↔ b ∈ ofColex l₂) ∧ a ∈ ofColex l₂ ∧ a ∉ ofColex l₁

theorem Finset.Colex.lt_iff_pi_lex_lt_pi_lex {α : Type u_4} {π : α → Type u_3} [LinearOrder α] [(a : α) → PartialOrder (π a)] (f g : (a : α) → π a) (h : ∀ (a : α), f a > g a) (l₁ l₂ : Colex (Finset α)) : l₁ < l₂ ↔ Pi.Lex (fun (x1 x2 : α) => x1 > x2) (fun {i : α} (x1 x2 : π i) => x1 < x2) ((ofColex l₁).piecewise f g) ((ofColex l₂).piecewise f g)

theorem Finset.Colex.strictMono_toColex_piecewise_ofColex {α : Type u_4} {π : α → Type u_3} [LinearOrder α] [(a : α) → PartialOrder (π a)] (f g : (a : α) → π a) (h : ∀ (a : α), f a > g a) : StrictMono fun (l : Colex (Finset α)) => toColex ((ofColex l).piecewise f g)

instance Finset.Colex.wellFoundedLT {α : Type u_3} [LinearOrder α] [WellFoundedLT α] : WellFoundedLT (Colex (Finset α))

theorem MonomialOrder.toWithBotSyn_monotone {σ : Type u_1} {m : MonomialOrder σ} : Monotone ⇑m.toWithBotSyn

theorem MonomialOrder.withBotDegree_le_coe_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] (f : MvPolynomial σ R) : m.withBotDegree f ≤ ↑(m.degree f)

theorem MonomialOrder.notMem_support_of_degree_lt' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] {a : σ →₀ ℕ} {f : MvPolynomial σ R} (h : m.toSyn (m.degree f) < m.toSyn a) : a ∉ f.support

theorem Set.ofPred_mem_range {α : Type u_3} {ι : Type u_4} {p : α → Prop} {f : ι → α} : {a : α | a ∈ range f ∧ p a} = f '' {i : ι | p (f i)}

theorem MonomialOrder.degree_le_of_withBotDegree_le_coe {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] {e : m.syn} {f : MvPolynomial σ R} (h : m.toWithBotSyn (m.withBotDegree f) ≤ ↑e) : m.toSyn (m.degree f) ≤ e

theorem MonomialOrder.coeff_mul_of_degree_add_degree_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] {e : σ →₀ ℕ} {f g : MvPolynomial σ R} [Decidable (m.degree f + m.degree g = e)] (h : m.toSyn (m.degree f + m.degree g) ≤ m.toSyn e) : (f * g).coeff e = if m.degree f + m.degree g = e then m.leadingCoeff f * m.leadingCoeff g else 0

theorem MonomialOrder.coeff_mul_of_withBotDegree_add_withBotDegree_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] {e : σ →₀ ℕ} {f g : MvPolynomial σ R} [Decidable (m.withBotDegree f + m.withBotDegree g = ↑e)] (h : m.toWithBotSyn (m.withBotDegree f + m.withBotDegree g) ≤ m.toWithBotSyn ↑e) : (f * g).coeff e = if m.withBotDegree f + m.withBotDegree g = ↑e then m.leadingCoeff f * m.leadingCoeff g else 0

theorem Finsupp.support_mapRange' {α : Type u_3} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] {f : M → N} {hf : f 0 = 0} {g : α →₀ M} (h : ∀ (x : M), f x = 0 → x = 0) : (mapRange f hf g).support = g.support

theorem MonomialOrder.monomial_mem_span_range_leadingTerm_tfae {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} {ι : Type u_4} [CommSemiring R] {e : σ →₀ ℕ} {c : R} {b : ι → MvPolynomial σ R} : [(MvPolynomial.monomial e) c ∈ Ideal.span (Set.range (m.leadingTerm ∘ b)), c ≠ 0 → ∃ (cs : ι →₀ R), (∀ i ∈ cs.support, m.degree (b i) ≤ e) ∧ c = (Finsupp.linearCombination R (m.leadingCoeff ∘ b)) cs, ∃ (g : ι →₀ MvPolynomial σ R), (∀ (i : ι), m.toWithBotSyn (m.withBotDegree (b i) + m.withBotDegree (g i)) ≤ m.toWithBotSyn ↑e) ∧ (MvPolynomial.monomial e) c = (Finsupp.linearCombination (MvPolynomial σ R) (m.leadingTerm ∘ b)) g, ∃ (g : ι →₀ MvPolynomial σ R), (∀ (i : ι), m.toWithBotSyn (m.withBotDegree (b i) + m.withBotDegree (g i)) ≤ m.toWithBotSyn ↑e) ∧ (MvPolynomial.monomial e) c = m.leadingTerm ((Finsupp.linearCombination (MvPolynomial σ R) b) g)].TFAE

theorem Finset.Colex.exists_mem_le_of_le_of_mem {α : Type u_3} [PartialOrder α] {l₁ l₂ : Colex (Finset α)} {a : α} (hle : l₁ ≤ l₂) (hmem : a ∈ ofColex l₁) : ∃ b ∈ ofColex l₂, a ≤ b

theorem Finset.Colex.max_le_max_of_le {α : Type u_3} [LinearOrder α] {l₁ l₂ : Colex (Finset α)} (h : l₁ ≤ l₂) : (ofColex l₁).max ≤ (ofColex l₂).max

theorem MonomialOrder.withBotDegree_le_withBotDegree_of_toColex_support_le_toColex_support {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_3} [CommSemiring R] {f g : MvPolynomial σ R} (h : toColex (Finset.image (⇑m.toSyn) f.support) ≤ toColex (Finset.image (⇑m.toSyn) g.support)) : m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g)

theorem MonomialOrder.toColex_support_sub_lt_toColex_support {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {e : σ →₀ ℕ} {f g : MvPolynomial σ R} (he : e ∈ f.support) (h : m.leadingTerm g = (MvPolynomial.monomial e) (f.coeff e)) : toColex (Finset.image (⇑m.toSyn) (f - g).support) < toColex (Finset.image (⇑m.toSyn) f.support)

theorem MonomialOrder.toColex_support_sub_le_toColex_support {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {e : σ →₀ ℕ} {f g : MvPolynomial σ R} (h : m.leadingTerm g = (MvPolynomial.monomial e) (f.coeff e)) : toColex (Finset.image (⇑m.toSyn) (f - g).support) ≤ toColex (Finset.image (⇑m.toSyn) f.support)

theorem MonomialOrder.withBotDegree_sub_le_withBotDegree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {e : σ →₀ ℕ} {f g : MvPolynomial σ R} (h : m.leadingTerm g = (MvPolynomial.monomial e) (f.coeff e)) : m.toWithBotSyn (m.withBotDegree (f - g)) ≤ m.toWithBotSyn (m.withBotDegree f)

theorem MonomialOrder.weakDiv {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {ι : Type u_3} {b : ι → MvPolynomial σ R} (f : MvPolynomial σ R) : ∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧ (∀ (i : ι), m.toWithBotSyn (m.withBotDegree (b i) + m.withBotDegree (g i)) ≤ m.toWithBotSyn (m.withBotDegree f)) ∧ ∀ e ∈ r.support, (MvPolynomial.monomial e) (r.coeff e) ∉ Ideal.span (Set.range (m.leadingTerm ∘ b))

theorem MonomialOrder.weakDiv_set {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {B : Set (MvPolynomial σ R)} (f : MvPolynomial σ R) : ∃ (g : ↑B →₀ MvPolynomial σ R) (r : MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) g + r ∧ (∀ (b : ↑B), m.toWithBotSyn (m.withBotDegree ↑b + m.withBotDegree (g b)) ≤ m.toWithBotSyn (m.withBotDegree f)) ∧ ∀ e ∈ r.support, (MvPolynomial.monomial e) (r.coeff e) ∉ Ideal.span (m.leadingTerm '' B)