Remainder

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

• MonomialOrder.IsRemainder m f B r: Given a multivariate polynomial f and a set B of multivariate polynomials over a commutative semiring R, with respect to a monomial order m. A polynomial r is called a remainder of f on division by B if there exists: (1) A finite linear combination: f = ∑ (g(b) * b) + r where g : B →₀ R[X] (finitely supported coefficients). (2) Degree condition: For each b ∈ B, the degree of g(b) * b is ≤ the degree of f under 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 variant equivalent statements.

• 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_range: A variant of MonomialOrder.IsRemainder where divisors are given as a family of polynomials.

Naming convention

Some theorems with an argument in type Set (MvPolynomial σ R) have 2 variants, named as following respectively:

• without suffix ' or ₀: leading coefficients of all polynomials in the set are non-zero divisors · ∈ nonZeroDivisors (MvPolynomial σ R) (or invertible IsUnit ·, depending on the theorem);
• with suffix ₀: leading coefficients of echo polynomial in the set is non-zero divisors (or invertible) or 0 · = 0.

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.

This definition makes sense only when R is a communitive ring and any polynomial in B has an invertible or zero leading coefficient.

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 : MvPolynomial σ R →₀ MvPolynomial σ R), ↑g.support ⊆ B ∧ p = (Finsupp.linearCombination (MvPolynomial σ R) id) g + r ∧ ∀ b ∈ B, m.toWithBotSyn (m.withBotDegree (b * 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' * 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' * 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_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 * 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.

@[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_leadingTerm {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)) (h : m.IsRemainder p B r) (s : σ →₀ ℕ) : s ∈ r.support → (MvPolynomial.monomial s) (MvPolynomial.coeff s r) ∉ Ideal.span (m.leadingTerm '' B)

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)} (hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0) (h : m.IsRemainder p B r) (s : σ →₀ ℕ) : s ∈ r.support → (MvPolynomial.monomial s) (MvPolynomial.coeff s r) ∉ Ideal.span (m.leadingTerm '' B)

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

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

theorem MonomialOrder.IsRemainder.monomial_notMem_span_leadingTerm₀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p r : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} (hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p) ∨ p = 0) (h : m.IsRemainder p B r) (s : σ →₀ ℕ) : s ∈ r.support → (MvPolynomial.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} (hB : ∀ b ∈ B, m.leadingCoeff b ∈ nonZeroDivisors R) (h : m.IsRemainder f B r) : m.toWithBotSyn (m.withBotDegree r) ≤ m.toWithBotSyn (m.withBotDegree f)

theorem MonomialOrder.IsRemainder.exists_withBotDegree_le_degree {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {B : Set (MvPolynomial σ R)} {r : MvPolynomial σ R} (hB : ∀ b ∈ B, m.leadingCoeff b ∈ nonZeroDivisors 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_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) (hB : ∀ b ∈ B, m.leadingCoeff b ∈ nonZeroDivisors R) (h : m.IsRemainder p B 0) : ∃ b ∈ B, m.degree b ≤ m.degree 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) (hB : ∀ b ∈ B, m.leadingCoeff b ∈ nonZeroDivisors R ∨ b = 0) (h : m.IsRemainder p B 0) : ∃ b ∈ B, b ≠ 0 ∧ 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.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

A variant of MonomialOrder.div_set using MonomialOrder.IsRemainder.

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} (hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)) (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

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

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