Resultants of monic polynomials and entire power series

Let P be a monic polynomial of degree d over a complete normed commutative ring R. Division by P sends an entire series F to a remainder F %ₘ P of degree less than d (PowerSeries.modByMonic), and hence to an element of the finite free R-algebra R[X] ⧸ (P) = AdjoinRoot P of rank d. The entire resultant Res(P, F) is the determinant of multiplication by this element, that is, its norm Algebra.norm R. For a polynomial F it is the classical resultant of P and F, and if P = ∏ (X - aᵢ) it is the product ∏ F(aᵢ) of the values of F at the roots of P.

Over an ultrametric ring with ‖1‖ = 1, division is unique, so reduction modulo P is a ring homomorphism from entire series onto AdjoinRoot P with kernel P times the entire series (PowerSeries.IsEntire.mkAdjoinRoot, in TauCeti.RingTheory.PowerSeries.Entire.Division), and the entire resultant is the norm of this reduction. It is then multiplicative in F, depends only on F modulo P, and is a unit exactly when P and F are coprime in the ring of entire series. It satisfies a Bézout identity Res(P, F) = P * G + H * F with G entire and H a polynomial of degree less than d.

These are the algebraic identities through which entire series, such as the Fredholm determinants of compact operators, are reduced modulo polynomial factors.

Main definitions

• Polynomial.entireResultant: the resultant Res(P, F) of a polynomial and a power series.

Main results

• Polynomial.entireResultant_coe: on polynomials, the entire resultant is the polynomial resultant, read at any degree bound for the second argument.
• Polynomial.entireResultant_eq_prod_evalAt: if P = ∏ (X - aᵢ), then Res(P, F) = ∏ F(aᵢ); in particular Res(X - a, F) = F(a) (Polynomial.entireResultant_X_sub_C).
• Polynomial.entireResultant_map: compatibility with continuous coefficient homomorphisms.
• Polynomial.tendsto_entireResultant_trunc: the entire resultant is the limit of the resultants of the polynomial truncations.
• Polynomial.entireResultant_add_mul and Polynomial.entireResultant_mul: invariance modulo P and multiplicativity in F.
• Polynomial.exists_C_entireResultant_eq: the Bézout identity Res(P, F) = P * G + H * F.
• Polynomial.isUnit_entireResultant_iff: Res(P, F) is a unit exactly when P and F are coprime in the ring of entire series.

References

• R. F. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), Appendix A3.

noncomputable def Polynomial.entireResultant {R : Type u_1} [CommRing R] [TopologicalSpace R] (P : Polynomial R) (F : PowerSeries R) : R

The entire resultant Res(P, F) of a polynomial P and a power series F: the norm over R of the class of the remainder F.modByMonic P in AdjoinRoot P, that is, the determinant of multiplication by that remainder on R[X] ⧸ (P). It is meaningful for monic P and entire F, when F is congruent to its remainder modulo P (PowerSeries.IsEntire.modByMonic_add_divByMonic).

theorem Polynomial.entireResultant_def {R : Type u_1} [CommRing R] [TopologicalSpace R] (P : Polynomial R) (F : PowerSeries R) : P.entireResultant F = (Algebra.norm R) ((AdjoinRoot.mk P) (F.modByMonic P))

The entire resultant is the norm of the class of the remainder.

theorem Polynomial.entireResultant_eq_resultant {R : Type u_1} [CommRing R] [TopologicalSpace R] {P : Polynomial R} (hP : P.Monic) (F : PowerSeries R) : P.entireResultant F = P.resultant (F.modByMonic P)

For monic P, the entire resultant of P and F is the polynomial resultant of P and the remainder of F.

theorem Polynomial.entireResultant_eq_resultant_of_natDegree_le {R : Type u_1} [CommRing R] [TopologicalSpace R] {P : Polynomial R} (hP : P.Monic) {F : PowerSeries R} {n : ℕ} (hn : (F.modByMonic P).natDegree ≤ n) : P.entireResultant F = P.resultant (F.modByMonic P) P.natDegree n

For monic P, the entire resultant of P and F is the polynomial resultant of P and the remainder of F, read at any degree bound for the remainder.

@[simp]

theorem Polynomial.entireResultant_one_left {R : Type u_1} [CommRing R] [TopologicalSpace R] (F : PowerSeries R) : entireResultant 1 F = 1

The resultant with the polynomial 1 is 1: the quotient algebra R[X] ⧸ (1) has rank zero. This holds for every F, including F = 0.

@[simp]

theorem Polynomial.entireResultant_zero_right {R : Type u_1} [CommRing R] [TopologicalSpace R] {P : Polynomial R} (hP : P.Monic) : P.entireResultant 0 = 0 ^ P.natDegree

The resultant of a monic P with 0 is 0 ^ deg P: it vanishes unless P = 1.

theorem Polynomial.entireResultant_coe {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {P : Polynomial R} (hP : P.Monic) (g : Polynomial R) {n : ℕ} (hn : g.natDegree ≤ n) : P.entireResultant ↑g = P.resultant g P.natDegree n

Agreement with the polynomial resultant. For monic P and a polynomial g, the entire resultant is the resultant of P and g, read at any degree bound n for g.

@[simp]

theorem Polynomial.entireResultant_one_right {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {P : Polynomial R} (hP : P.Monic) : P.entireResultant 1 = 1

The resultant of a monic P with 1 is 1: multiplication by 1 has determinant 1.

@[simp]

theorem Polynomial.entireResultant_self {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {P : Polynomial R} (hP : P.Monic) : P.entireResultant ↑P = 0 ^ P.natDegree

The resultant of a monic P with itself is 0 ^ deg P: it vanishes unless P = 1.

theorem Polynomial.entireResultant_eq_prod_evalAt {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {P : Polynomial R} {F : PowerSeries R} {ι : Type u_2} [Fintype ι] {a : ι → R} (hP : P = ∏ i : ι, (X - C (a i))) (hF : F.IsEntire) : P.entireResultant F = ∏ i : ι, F.evalAt (a i)

The entire resultant at a split polynomial. If P = ∏ i, (X - aᵢ), then Res(P, F) is the product ∏ i, F(aᵢ) of the values of the entire series F at the roots of P. The roots may repeat.

@[simp]

theorem Polynomial.entireResultant_X_sub_C {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {F : PowerSeries R} (a : R) (hF : F.IsEntire) : (X - C a).entireResultant F = F.evalAt a

The resultant with a linear factor is a value: Res(X - a, F) = F(a) for entire F.

theorem Polynomial.entireResultant_map {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {P : Polynomial R} {F : PowerSeries R} {S : Type u_2} [CommRing S] [TopologicalSpace S] [T2Space S] (hP : P.Monic) (hF : F.IsEntire) (φ : R →+* S) (hφ : Continuous ⇑φ) : (map φ P).entireResultant ((PowerSeries.map φ) F) = φ (P.entireResultant F)

Base change. A continuous coefficient homomorphism φ carries the entire resultant of P and F to that of their images.

theorem Polynomial.tendsto_entireResultant_trunc {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {P : Polynomial R} {F : PowerSeries R} (hP : P.Monic) (hF : F.IsEntire) : Filter.Tendsto (fun (N : ℕ) => P.entireResultant ↑((PowerSeries.trunc N) F)) Filter.atTop (nhds (P.entireResultant F))

Continuity along truncations. For monic P and entire F, the resultants of P with the polynomial truncations of F converge to Res(P, F).

theorem Polynomial.exists_C_entireResultant_eq {R : Type u_1} [NormedCommRing R] [CompleteSpace R] {P : Polynomial R} {F : PowerSeries R} (hP : P.Monic) (hF : F.IsEntire) : ∃ (G : PowerSeries R), G.IsEntire ∧ ∃ (H : Polynomial R), H.degree < ↑P.natDegree ∧ PowerSeries.C (P.entireResultant F) = ↑P * G + ↑H * F

The Bézout identity for the entire resultant. For monic P and entire F there are an entire series G and a polynomial H of degree less than deg P with Res(P, F) = P * G + H * F.

theorem Polynomial.entireResultant_eq_norm_mkAdjoinRoot {R : Type u_1} [NormedCommRing R] [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] {P : Polynomial R} (hP : P.Monic) (F : ↥(PowerSeries.IsEntire.subring R)) : P.entireResultant ↑F = (Algebra.norm R) ((PowerSeries.IsEntire.mkAdjoinRoot hP) F)

The entire resultant of P and F is the norm of the reduction of F modulo P.

theorem Polynomial.entireResultant_add_mul {R : Type u_1} [NormedCommRing R] [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] {P : Polynomial R} {F G : PowerSeries R} (hP : P.Monic) (hF : F.IsEntire) (hG : G.IsEntire) : P.entireResultant (F + ↑P * G) = P.entireResultant F

Invariance modulo P. The entire resultant Res(P, F) depends only on F modulo P.

theorem Polynomial.entireResultant_mul {R : Type u_1} [NormedCommRing R] [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] {P : Polynomial R} {F G : PowerSeries R} (hP : P.Monic) (hF : F.IsEntire) (hG : G.IsEntire) : P.entireResultant (F * G) = P.entireResultant F * P.entireResultant G

Multiplicativity. Res(P, F * G) = Res(P, F) * Res(P, G) for entire F and G.

theorem Polynomial.isUnit_entireResultant_iff {R : Type u_1} [NormedCommRing R] [CompleteSpace R] [IsUltrametricDist R] [NormOneClass R] {P : Polynomial R} {F : PowerSeries R} (hP : P.Monic) (hF : F.IsEntire) : IsUnit (P.entireResultant F) ↔ IsCoprime ⟨↑P, ⋯⟩ ⟨F, ⋯⟩

The entire resultant detects coprimality. For monic P and entire F, Res(P, F) is a unit exactly when P and F are coprime in the ring of entire series.