Remainder

The following definition is abstracted from the "remainder" as in MonomialOrder.div_set. And more properties of it is covered in this file.

• MonomialOrder.IsRemainder m f B r: Given a multivariate polynomial f and a "divisors" set B of with respect to a monomial order m. A polynomial r is called a remainder of f on division by B if there exists:

  1. Finite linear combination: f = ∑ (g(b) * b) + r;
  2. Degree condition: For each b ∈ B, the degree (with bot) of g(b) * b ≤ the degree (with bot) of f w.r.t. monomial order m;
  3. Remainder irreducibility: No term of r is divisible by the leading monomial of any non-zero b ∈ B.

And there're also some equivalent variants.

• MonomialOrder.IsRemainder.isRemainder_def': A variant of MonomialOrder.IsRemainder without coercion of a Set (MvPolynomial σ R).

• MonomialOrder.IsRemainder.isRemainder_def'': A variant of MonomialOrder.IsRemainder where g : MvPolynomial σ R →₀ MvPolynomial σ R is replaced with a function g : MvPolynomial σ R → MvPolynomial σ R without limitation on its support.

• MonomialOrder.IsRemainder.isRemainder_def_degree: A variant where the degree condition is formalized with m.degree, which matches the statement of MonomialOrder.div_set.

• MonomialOrder.IsRemainder.isRemainder_range: A variant of MonomialOrder.IsRemainder where divisors are given as a family of polynomials.

There exists a remainder when the polynomial ring is communitive and any divisor either has an invertible leading coefficient or is 0.

• MonomialOrder.IsRemainder.exists_isRemainder.

Naming convention

Some theorems with an argument in type Set (MvPolynomial σ R) and a hypothesis that leading coefficients of all polynomials in the set are invertible have 2 variants, named as following respectively:

• without suffix ' or ₀: any polynomial b in the set has an invertible leading coefficient (IsUnit (m.leadingCoeff p));
• with suffix ₀: any polynomial b in the set either has an invertible leading coefficient or is equal to 0 (IsUnit (m.leadingCoeff p) ∨ b = 0);
• with suffix ': no hypotheses on leading coefficients, while requiring R to be a field (Field k, where the ring is denoted as k instead).

Implementation notes

The definition of remainder makes sense when R is a communitive ring and any polynomial in B either has an invertible leading coefficient or is 0, while for simplicity we try to formalize it without applying these restrictions as its hypotheses.

We try to adjust its formal definition s.t. it corresponds with the informal definition well when the above condition holds, while keeps simple and still shares some common properties without these hypotheses.

• Degree condition is formalized as

  m.toWithBotSyn (m.withBotDegree b.val) + m.toWithBotSyn (m.withBotDegree (g b)) ≤
    m.toWithBotSyn (m.withBotDegree f)
  

  instead of m.withBotDegree (b.val * g b) ≼'[m] m.withBotDegree f.

  If IsRemainder was formalized with the latter one, some properties would require polynomials in B to have non-zero divisor leading coefficients since they need m.withBotDegree (b.val * g b) = m.withBotDegree (b.val) + m.withBotDegree (g b) with this formalization of IsRemainder. They no longer require this if IsRemainder is formalized with former one.

• Remainder irreducibility is formalized as ∀ c ∈ r.support, ∀ b ∈ B, b ≠ 0 → ¬ (m.degree b ≤ c), where ¬ (m.degree b ≤ c) is sufficient but unnecessary for the indivisibility between the leading term of b (m.leadingTerm b) and the term of r with exponents c (monomial c (b.coeff c)).

Reference : [Cox2015]

def MonomialOrder.IsRemainder {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) : Prop

Given a multivariate polynomial f and a set B of multivariate polynomials over R. A polynomial r is called a remainder of f on division by B with respect to a monomial order m, if there exists g : B →₀ R[X] and a polynomial r s.t.

1. Finite linear combination: f = ∑ (g(b) * b) + r;
2. Degree condition: For eacho b ∈ B, the degree (with bot) of g(b) * b ≤ the degree (with bot) of f w.r.t. m;
3. Remainder irreducibility: No term of r is divisible by the leading monomial of any non-zero b ∈ B.

The definition of remainder makes sense when R is a communitive ring and any polynomial in B either has an invertible leading coefficient or is 0. See the implementation note for the formalization unaligned with the informal definition when not in this case.

Equations

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

theorem MonomialOrder.IsRemainder.isRemainder_def {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) : m.IsRemainder p B r ↔ (∃ (g : ↑B → MvPolynomial σ R) (B' : Finset ↑B), p = ∑ x ∈ B', g x * ↑x + r ∧ ∀ b ∈ B', m.toWithBotSyn (m.withBotDegree ↑b) + m.toWithBotSyn (m.withBotDegree (g b)) ≤ m.toWithBotSyn (m.withBotDegree p)) ∧ ∀ c ∈ r.support, ∀ g' ∈ B, g' ≠ 0 → ¬m.degree g' ≤ c

theorem MonomialOrder.IsRemainder.isRemainder_def' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) : m.IsRemainder p B r ↔ (∃ (g : MvPolynomial σ R →₀ MvPolynomial σ R), ↑g.support ⊆ B ∧ p = (Finsupp.linearCombination (MvPolynomial σ R) id) g + r ∧ ∀ b ∈ B, m.toWithBotSyn (m.withBotDegree b) + m.toWithBotSyn (m.withBotDegree (g b)) ≤ m.toWithBotSyn (m.withBotDegree p)) ∧ ∀ c ∈ r.support, ∀ g' ∈ B, g' ≠ 0 → ¬m.degree g' ≤ c

A variant of MonomialOrder.IsRemainder without coercion of a Set (MvPolynomial σ R).

theorem MonomialOrder.IsRemainder.isRemainder_def'' {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) : m.IsRemainder p B r ↔ (∃ (g : MvPolynomial σ R → MvPolynomial σ R) (B' : Finset (MvPolynomial σ R)), ↑B' ⊆ B ∧ p = ∑ x ∈ B', g x * x + r ∧ ∀ b' ∈ B', m.toWithBotSyn (m.withBotDegree b') + m.toWithBotSyn (m.withBotDegree (g b')) ≤ m.toWithBotSyn (m.withBotDegree p)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, b ≠ 0 → ¬m.degree b ≤ c

A variant of MonomialOrder.IsRemainder where g : MvPolynomial σ R →₀ MvPolynomial σ R is replaced with a function g : MvPolynomial σ R → MvPolynomial σ R without limitation on its support.

theorem MonomialOrder.IsRemainder.isRemainder_finset {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B' : Finset (MvPolynomial σ R)) (r : MvPolynomial σ R) : m.IsRemainder p (↑B') r ↔ (∃ (g : MvPolynomial σ R → MvPolynomial σ R), p = ∑ x ∈ B', g x * x + r ∧ ∀ b' ∈ B', m.toWithBotSyn (m.withBotDegree b') + m.toWithBotSyn (m.withBotDegree (g b')) ≤ m.toWithBotSyn (m.withBotDegree p)) ∧ ∀ c ∈ r.support, ∀ b ∈ B', b ≠ 0 → ¬m.degree b ≤ c

A variant of MonomialOrder.IsRemainder_def' where B is Finset (MvPolynomial σ R).

theorem MonomialOrder.IsRemainder.isRemainder_iff_exists_isRemainder_finset {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) : m.IsRemainder p B r ↔ (∃ (B' : Finset (MvPolynomial σ R)), ↑B' ⊆ B ∧ m.IsRemainder p (↑B') r) ∧ ∀ c ∈ r.support, ∀ b ∈ B, b ≠ 0 → ¬m.degree b ≤ c

theorem MonomialOrder.IsRemainder.isRemainder_range {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {ι : Type u_3} (f : MvPolynomial σ R) (b : ι → MvPolynomial σ R) (r : MvPolynomial σ R) : m.IsRemainder f (Set.range b) r ↔ (∃ (g : ι →₀ MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧ ∀ (i : ι), m.toWithBotSyn (m.withBotDegree (b i)) + m.toWithBotSyn (m.withBotDegree (g i)) ≤ m.toWithBotSyn (m.withBotDegree f)) ∧ ∀ c ∈ r.support, ∀ (i : ι), b i ≠ 0 → ¬m.degree (b i) ≤ c

r is a remainder of a family of polynomials, if and only if it is a remainder with properities defined in MonomialOrder.div with this family of polynomials given as a map from indexes to them.

It is a variant of MonomialOrder.IsRemainder where divisors are given as a map from indexes to polynomials.

theorem MonomialOrder.IsRemainder.isRemainder_range_fintype {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) {ι : Type u_3} [Fintype ι] (b : ι → MvPolynomial σ R) (r : MvPolynomial σ R) : m.IsRemainder p (Set.range b) r ↔ (∃ (g : ι → MvPolynomial σ R), p = ∑ i : ι, b i * g i + r ∧ ∀ (i : ι), m.toWithBotSyn (m.withBotDegree (b i)) + m.toWithBotSyn (m.withBotDegree (g i)) ≤ m.toWithBotSyn (m.withBotDegree p)) ∧ ∀ c ∈ r.support, ∀ (i : ι), b i ≠ 0 → ¬m.degree (b i) ≤ c

@[simp]

theorem MonomialOrder.IsRemainder.isRemainder_insert_zero_iff_isRemainder {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) : m.IsRemainder p (insert 0 B) r ↔ m.IsRemainder p B r

Remainders are preserved on insertion of the zero polynomial into the set of divisors.

@[simp]

theorem MonomialOrder.IsRemainder.isRemainder_sdiff_singleton_zero_iff_isRemainder {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) : m.IsRemainder p (B \ {0}) r ↔ m.IsRemainder p B r

Remainders are preserved with the zero polynomial removed from the set of divisors.

theorem MonomialOrder.IsRemainder.isRemainder_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} (h : m.IsRemainder 0 B r) : r = 0

@[simp]

theorem MonomialOrder.IsRemainder.isRemainder_zero_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) : m.IsRemainder 0 B r ↔ r = 0

theorem MonomialOrder.IsRemainder.isRemainder_iff_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) (hB : ∀ b ∈ B, m.leadingCoeff b ∈ nonZeroDivisors R) : m.IsRemainder f B r ↔ (∃ (g : ↑B →₀ MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) g + r ∧ ∀ (b : ↑B), m.toSyn (m.degree (↑b * g b)) ≤ m.toSyn (m.degree f)) ∧ ∀ c ∈ r.support, ∀ b ∈ B, b ≠ 0 → ¬m.degree b ≤ c

theorem MonomialOrder.IsRemainder.mem_ideal_of_mem_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} {I : Ideal (MvPolynomial σ R)} {p : MvPolynomial σ R} (hBI : B ⊆ ↑I) (hpBr : m.IsRemainder p B r) (hr : r ∈ I) : p ∈ I

theorem MonomialOrder.IsRemainder.term_notMem_span_span_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (h : m.IsRemainder p B r) (s : σ →₀ ℕ) : s ∈ r.support → (MvPolynomial.monomial s) (MvPolynomial.coeff s r) ∉ Ideal.span ((fun (p : MvPolynomial σ R) => (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))

theorem MonomialOrder.IsRemainder.term_notMem_span_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (h : m.IsRemainder p B r) (s : σ →₀ ℕ) : s ∈ r.support → (MvPolynomial.monomial s) (MvPolynomial.coeff s r) ∉ Ideal.span (m.leadingTerm '' B)

theorem MvPolynomial.monomial_notMem_span_monomial {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (h : ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c) (s : σ →₀ ℕ) : s ∈ r.support → (monomial s) 1 ∉ Ideal.span ((fun (p : MvPolynomial σ R) => (monomial (m.degree p)) 1) '' B)

theorem MvPolynomial.monomial_notMem_span_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (h : ∀ c ∈ r.support, ∀ b ∈ B, ¬m.degree b ≤ c) (s : σ →₀ ℕ) : s ∈ r.support → (monomial s) 1 ∉ Ideal.span (m.leadingTerm '' B)

theorem MonomialOrder.IsRemainder.withBotDegree_remainder_le {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {f : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} (h : m.IsRemainder f B r) : m.toWithBotSyn (m.withBotDegree r) ≤ m.toWithBotSyn (m.withBotDegree f)

theorem MonomialOrder.IsRemainder.exists_withBotDegree_le_withBotDegree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} (h : m.IsRemainder p B r) (hfr : m.withBotDegree p ≠ m.withBotDegree r) : ∃ b ∈ B, m.withBotDegree b ≤ m.withBotDegree p

theorem MonomialOrder.IsRemainder.exists_withBotDegree_le_withBotDegree₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} (h : m.IsRemainder p B r) (hfr : m.withBotDegree p ≠ m.withBotDegree r) : ∃ b ∈ B, b ≠ 0 ∧ m.withBotDegree b ≤ m.withBotDegree p

theorem MonomialOrder.IsRemainder.withBotDegree_eq_withBotDegree_iff_leadingTerm_eq_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} (h : m.IsRemainder p B r) : m.withBotDegree r = m.withBotDegree p ↔ m.leadingTerm r = m.leadingTerm p

theorem MonomialOrder.IsRemainder.exists_degree_le_degree_of_zero {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (hp : p ≠ 0) (h : m.IsRemainder p B 0) : ∃ b ∈ B, m.degree b ≤ m.degree p

@[simp]

theorem MonomialOrder.IsRemainder.of_subsingleton {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] [Subsingleton (MvPolynomial σ R)] {p r : MvPolynomial σ R} {s : Set (MvPolynomial σ R)} : m.IsRemainder p s r

theorem MonomialOrder.Embedding.isRemainder_killCompl_of_isRemainder_rename {R : Type u_2} [CommSemiring R] {σ' : Type u_3} {σ : Type u_4} {m' : MonomialOrder σ'} {m : MonomialOrder σ} (e : m'.Embedding m) {p : MvPolynomial σ' R} {B : Set (MvPolynomial σ' R)} {r : MvPolynomial σ R} (h : m.IsRemainder ((MvPolynomial.rename ⇑e) p) (⇑(MvPolynomial.rename ⇑e) '' B) r) : m'.IsRemainder p B ((MvPolynomial.killCompl ⋯) r)

theorem MonomialOrder.Embedding.isRemainder_rename_of_isRemainder {R : Type u_2} [CommSemiring R] {σ' : Type u_3} {σ : Type u_4} {m' : MonomialOrder σ'} {m : MonomialOrder σ} (e : m'.Embedding m) {p : MvPolynomial σ' R} {B : Set (MvPolynomial σ' R)} {r : MvPolynomial σ' R} (h : m'.IsRemainder p B r) : m.IsRemainder ((MvPolynomial.rename ⇑e) p) (⇑(MvPolynomial.rename ⇑e) '' B) ((MvPolynomial.rename ⇑e) r)

theorem MonomialOrder.Embedding.isRemainder_iff_isRemainder_rename {R : Type u_2} [CommSemiring R] {σ' : Type u_3} {σ : Type u_4} {m' : MonomialOrder σ'} {m : MonomialOrder σ} (e : m'.Embedding m) (p : MvPolynomial σ' R) {B : Set (MvPolynomial σ' R)} (r : MvPolynomial σ' R) : m'.IsRemainder p B r ↔ m.IsRemainder ((MvPolynomial.rename ⇑e) p) (⇑(MvPolynomial.rename ⇑e) '' B) ((MvPolynomial.rename ⇑e) r)

theorem MonomialOrder.IsRemainder.exists_isRemainder {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {B : Set (MvPolynomial σ R)} (hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b)) (p : MvPolynomial σ R) : ∃ (r : MvPolynomial σ R), m.IsRemainder p B r

theorem MonomialOrder.IsRemainder.exists_isRemainder₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {B : Set (MvPolynomial σ R)} (hB : ∀ b ∈ B, IsUnit (m.leadingCoeff b) ∨ b = 0) (p : MvPolynomial σ R) : ∃ (r : MvPolynomial σ R), m.IsRemainder p B r

A variant of div_set' including 0

theorem MonomialOrder.IsRemainder.mem_ideal_iff {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} {I : Ideal (MvPolynomial σ R)} {p : MvPolynomial σ R} (hBI : B ⊆ ↑I) (hpBr : m.IsRemainder p B r) : r ∈ I ↔ p ∈ I

theorem MonomialOrder.IsRemainder.sub_mem_ideal_of_isRemainder_of_subset_ideal {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {B : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} {p r₁ r₂ : MvPolynomial σ R} (hBI : B ⊆ ↑I) (hr₁ : m.IsRemainder p B r₁) (hr₂ : m.IsRemainder p B r₂) : r₁ - r₂ ∈ I

theorem MonomialOrder.IsRemainder.sub_monomial_notMem_span_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {B : Set (MvPolynomial σ R)} {p r₁ r₂ : MvPolynomial σ R} (hr₁ : m.IsRemainder p B r₁) (hr₂ : m.IsRemainder p B r₂) (s : σ →₀ ℕ) : s ∈ (r₁ - r₂).support → (MvPolynomial.monomial s) 1 ∉ Ideal.span (m.leadingTerm '' B)

theorem MonomialOrder.IsRemainder.exists_isRemainder' {k : Type u_1} [Field k] {σ : Type u_2} {m : MonomialOrder σ} (B : Set (MvPolynomial σ k)) (p : MvPolynomial σ k) : ∃ (r : MvPolynomial σ k), m.IsRemainder p B r

A variant of div_set' in field