Polynomial reducta

The reductum p.reductum k retains exactly the terms of p of degree strictly below k. The finite set p.reducta contains the reducta at every cutoff through p.natDegree + 1, so it includes both zero and p itself. After any coefficient specialization, one member of this set maps to the specialized polynomial: take the cutoff immediately above its new degree. This is the finite degree-case decomposition needed when polynomial degrees can drop under specialization.

The reductum is PowerSeries.trunc applied to p viewed as a power series. Reducta also agree with repeatedly deleting leading terms, connecting the fixed cutoffs used for specialization to Mathlib's eraseLead API.

Main results

• Polynomial.coeff_reductum: a reductum keeps precisely the coefficients below its cutoff.
• Polynomial.reductum_reductum: nested reducta reduce to the smaller cutoff.
• Polynomial.derivative_reductum: differentiation lowers the cutoff by one.
• Polynomial.reductum_natDegree: the cutoff at the degree deletes the leading term.
• Polynomial.reducta_map: coefficient maps carry the reducta onto the reducta of the mapped polynomial, with no injectivity or degree-preservation hypothesis.
• Polynomial.exists_mem_reducta_map_eq: every coefficient specialization is the image of a reductum of the original polynomial.
• Polynomial.reducta_eq_eraseLeadOrbit: the bounded cutoffs give exactly the finite orbit under repeated deletion of leading terms.

References

• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 4 and 11.

noncomputable def Polynomial.reductum {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : Polynomial R

The part of p of degree strictly below k.

theorem Polynomial.reductum_eq_trunc {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : p.reductum k = (PowerSeries.trunc k) ↑p

A reductum is the truncation of p, viewed as a power series, at the same cutoff.

@[simp]

theorem Polynomial.coeff_reductum {R : Type u_1} [Semiring R] (p : Polynomial R) (k i : ℕ) : (p.reductum k).coeff i = if i < k then p.coeff i else 0

A reductum keeps the coefficients strictly below its cutoff and discards the rest.

theorem Polynomial.reductum_eq_sum {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : p.reductum k = ∑ i ∈ Finset.range k, (monomial i) (p.coeff i)

A reductum is the sum of the monomials of p below its cutoff.

@[simp]

theorem Polynomial.reductum_zero {R : Type u_1} [Semiring R] (p : Polynomial R) : p.reductum 0 = 0

The reductum at cutoff zero is zero.

@[simp]

theorem Polynomial.zero_reductum {R : Type u_1} [Semiring R] (k : ℕ) : reductum 0 k = 0

Every reductum of the zero polynomial is zero.

theorem Polynomial.reductum_succ {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : p.reductum (k + 1) = p.reductum k + (monomial k) (p.coeff k)

Increasing the cutoff by one adjoins the coefficient at the old cutoff.

theorem Polynomial.degree_reductum_lt {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : (p.reductum k).degree < ↑k

The degree of a reductum is strictly below its cutoff.

theorem Polynomial.natDegree_reductum_lt {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : (p.reductum (k + 1)).natDegree < k + 1

The natural degree of a reductum at a positive cutoff is strictly below that cutoff.

theorem Polynomial.reductum_eq_self {R : Type u_1} [Semiring R] {p : Polynomial R} {k : ℕ} (h : p.natDegree < k) : p.reductum k = p

A cutoff strictly above the degree does not change a polynomial.

@[simp]

theorem Polynomial.reductum_natDegree_add_one {R : Type u_1} [Semiring R] (p : Polynomial R) : p.reductum (p.natDegree + 1) = p

Cutting off immediately above the degree returns the original polynomial, including for zero.

@[simp]

theorem Polynomial.reductum_reductum {R : Type u_1} [Semiring R] (p : Polynomial R) (k l : ℕ) : (p.reductum l).reductum k = p.reductum (min k l)

Nested reducta use the minimum of their cutoffs.

theorem Polynomial.reductum_reductum_of_le {R : Type u_1} [Semiring R] (p : Polynomial R) {k l : ℕ} (h : k ≤ l) : (p.reductum l).reductum k = p.reductum k

Taking a smaller reductum after a larger one is the same as taking the smaller reductum directly.

@[simp]

theorem Polynomial.reductum_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) (k : ℕ) : (map f p).reductum k = map f (p.reductum k)

Reducta commute with coefficient maps, with no degree-preservation hypothesis.

theorem Polynomial.derivative_reductum {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : derivative (p.reductum (k + 1)) = (derivative p).reductum k

Differentiating a reductum lowers its cutoff by one.

theorem Polynomial.reductum_natDegree {R : Type u_1} [Semiring R] (p : Polynomial R) : p.reductum p.natDegree = p.eraseLead

The reductum at the degree is Mathlib's operation deleting the leading term.

theorem Polynomial.reductum_eraseLead {R : Type u_1} [Semiring R] (p : Polynomial R) {k : ℕ} (h : k ≤ p.natDegree) : p.eraseLead.reductum k = p.reductum k

Below the degree of p, taking a reductum is unaffected by first deleting the leading term.

theorem Polynomial.reductum_eq_eraseLead_of_lt_of_le {R : Type u_1} [Semiring R] {p : Polynomial R} {k : ℕ} (h₁ : p.eraseLead.natDegree < k) (h₂ : k ≤ p.natDegree) : p.reductum k = p.eraseLead

A cutoff above the degree of p.eraseLead but not above the degree of p deletes exactly the leading term.

noncomputable def Polynomial.reducta {R : Type u_1} [Semiring R] (p : Polynomial R) : Finset (Polynomial R)

The finite set of all reducta at cutoffs from zero through one above the degree.

theorem Polynomial.mem_reducta {R : Type u_1} [Semiring R] {p q : Polynomial R} : q ∈ p.reducta ↔ ∃ (k : ℕ), p.reductum k = q

The members of reducta are exactly the reducta at arbitrary cutoffs: the cutoffs past the degree add nothing new.

@[simp]

theorem Polynomial.reductum_mem_reducta {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : p.reductum k ∈ p.reducta

The reductum at every cutoff belongs to the reducta, including cutoffs past the degree.

@[simp]

theorem Polynomial.zero_mem_reducta {R : Type u_1} [Semiring R] (p : Polynomial R) : 0 ∈ p.reducta

Zero belongs to the reducta of every polynomial.

@[simp]

theorem Polynomial.self_mem_reducta {R : Type u_1} [Semiring R] (p : Polynomial R) : p ∈ p.reducta

Every polynomial belongs to its own reducta.

theorem Polynomial.eraseLead_mem_reducta {R : Type u_1} [Semiring R] (p : Polynomial R) : p.eraseLead ∈ p.reducta

Deleting the leading term produces a member of the reducta.

@[simp]

theorem Polynomial.reducta_zero {R : Type u_1} [Semiring R] : reducta 0 = {0}

The only reductum of the zero polynomial is zero.

theorem Polynomial.reducta_eq_insert_eraseLead_reducta {R : Type u_1} [Semiring R] [DecidableEq (Polynomial R)] (p : Polynomial R) : p.reducta = insert p p.eraseLead.reducta

The reducta consist of p together with the reducta after deleting its leading term.

noncomputable def Polynomial.eraseLeadOrbit {R : Type u_1} [Semiring R] (p : Polynomial R) : Finset (Polynomial R)

The finite orbit obtained by repeatedly deleting leading terms, including the zero polynomial at the end.

theorem Polynomial.mem_eraseLeadOrbit {R : Type u_1} [Semiring R] {p q : Polynomial R} : q ∈ p.eraseLeadOrbit ↔ ∃ k ≤ p.support.card, eraseLead^[k] p = q

Membership in the eraseLead orbit is being one of the first p.support.card + 1 iterates of eraseLead on p.

@[simp]

theorem Polynomial.eraseLeadOrbit_zero {R : Type u_1} [Semiring R] : eraseLeadOrbit 0 = {0}

The orbit of zero under eraseLead is the singleton containing zero.

theorem Polynomial.eraseLeadOrbit_eq_insert {R : Type u_1} [Semiring R] [DecidableEq (Polynomial R)] (p : Polynomial R) : p.eraseLeadOrbit = insert p p.eraseLead.eraseLeadOrbit

The eraseLead orbit of a polynomial is the polynomial together with the orbit of the polynomial with its leading term deleted.

theorem Polynomial.reducta_eq_eraseLeadOrbit {R : Type u_1} [Semiring R] (p : Polynomial R) : p.reducta = p.eraseLeadOrbit

The finite set of reducta at bounded cutoffs is exactly the finite orbit under deletion of leading terms.

theorem Polynomial.iterate_eraseLead_mem_eraseLeadOrbit {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : eraseLead^[k] p ∈ p.eraseLeadOrbit

Every iterate of eraseLead on p lies in its eraseLead orbit, including the iterates past the point where the orbit reaches zero.

theorem Polynomial.reducta_map {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [DecidableEq (Polynomial S)] (f : R →+* S) (p : Polynomial R) : (map f p).reducta = Finset.image (map f) p.reducta

Coefficient maps carry all reducta exactly to the reducta of the mapped polynomial, with no injectivity or degree-preservation hypothesis.

theorem Polynomial.map_reductum_natDegree_map_add_one {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : map f (p.reductum ((map f p).natDegree + 1)) = map f p

Cutting off immediately above the degree after specialization maps back to the specialized polynomial. This gives an explicit member of p.reducta witnessing exists_mem_reducta_map_eq.

theorem Polynomial.natDegree_reductum_natDegree_map_add_one {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : (p.reductum ((map f p).natDegree + 1)).natDegree = (map f p).natDegree

Cutting off immediately above the degree after specialization gives a reductum whose own degree is the specialized degree, so formal degree bounds taken at this reductum are the actual degrees after specialization.

theorem Polynomial.exists_mem_reducta_map_eq {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial R) : ∃ q ∈ p.reducta, map f q = map f p

Every coefficient specialization is the image of a member of the original polynomial's finite set of reducta.