Monic divisors of a Weierstrass polynomial are Weierstrass polynomials

A Weierstrass polynomial W = X^d + ∑ c_j X^{d-1-j} over Conv K m with c_j(0) = 0 reduces to X^d under the residue map convResidue : Conv K m → K (map_weierstrassPolynomial). A monic divisor Q of W reduces to a monic divisor Q̄ of X^d in K[X]; comparing trailing degrees in Q̄ · Q̄' = X^d (natTrailingDegree_mul) forces the trailing degree of Q̄ to equal its degree, so all lower coefficients of Q̄ vanish (coeff_eq_zero_of_monic_dvd_X_pow), i.e. the lower coefficients of Q vanish at 0: Q is the Weierstrass polynomial of its own coefficients (exists_weierstrassPolynomial_of_monic_dvd). In the language of [GR65, Chapter II, §B]: since P(0, x_m) = x_m^d, the restriction to the axis of each monic factor is a power of x_m. Used for the irreducibility (Irreducible.lean) and the unique factorization (UFD.lean).

The coefficient field K is ℝ or ℂ ([RCLike K]).

noncomputable def Analytic.convResidue (K : Type u_1) [RCLike K] {m : ℕ} : ↥(Conv K m) →+* K

The residue map Conv K m → K, the constant coefficient.

Equations

• Analytic.convResidue K = MvPowerSeries.constantCoeff.comp (Analytic.Conv K m).val.toRingHom

@[simp]

theorem Analytic.convResidue_apply {K : Type u_1} [RCLike K] {m : ℕ} (c : ↥(Conv K m)) : (convResidue K) c = MvPowerSeries.constantCoeff ↑c

theorem Analytic.map_weierstrassPolynomial {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] (f : R →+* S) (d : ℕ) (c : Fin d → R) : Polynomial.map f (weierstrassPolynomial d c) = weierstrassPolynomial d fun (j : Fin d) => f (c j)

Ring maps act on Weierstrass polynomials coefficientwise.

theorem Analytic.coeff_eq_zero_of_monic_dvd_X_pow {K : Type u_1} [RCLike K] {a : Polynomial K} (ha : a.Monic) {d : ℕ} (hdvd : a ∣ Polynomial.X ^ d) {i : ℕ} (hi : i < a.natDegree) : a.coeff i = 0

A monic divisor of X^d over K has vanishing coefficients below its degree (compare trailing degrees).

theorem Analytic.constantCoeff_coeff_eq_zero_of_map_dvd_X_pow {K : Type u_1} [RCLike K] {m : ℕ} {Q : Polynomial ↥(Conv K m)} (hQ : Q.Monic) {d : ℕ} (hmap : Polynomial.map (convResidue K) Q ∣ Polynomial.X ^ d) {i : ℕ} (hi : i < Q.natDegree) : MvPowerSeries.constantCoeff ↑(Q.coeff i) = 0

If the residue of a monic Q divides X^d, the coefficients of Q below its degree vanish at 0.

theorem Analytic.exists_weierstrassPolynomial_of_monic_dvd {K : Type u_1} [RCLike K] {m d : ℕ} {c : Fin d → ↥(Conv K m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) {Q : Polynomial ↥(Conv K m)} (hQ : Q.Monic) (hdvd : Q ∣ weierstrassPolynomial d c) : ∃ (d' : ℕ) (c' : Fin d' → ↥(Conv K m)), (∀ (j : Fin d'), MvPowerSeries.constantCoeff ↑(c' j) = 0) ∧ Q = weierstrassPolynomial d' c'

A monic divisor in (Conv K m)[X] of a Weierstrass polynomial is a Weierstrass polynomial (its lower coefficients vanish at 0) [GR65, Chapter II, §B].

theorem Analytic.exists_weierstrassPolynomial_mul {K : Type u_1} [RCLike K] {m d₁ d₂ : ℕ} {c₁ : Fin d₁ → ↥(Conv K m)} {c₂ : Fin d₂ → ↥(Conv K m)} (hc₁ : ∀ (j : Fin d₁), MvPowerSeries.constantCoeff ↑(c₁ j) = 0) (hc₂ : ∀ (j : Fin d₂), MvPowerSeries.constantCoeff ↑(c₂ j) = 0) : ∃ (c : Fin (d₁ + d₂) → ↥(Conv K m)), (∀ (j : Fin (d₁ + d₂)), MvPowerSeries.constantCoeff ↑(c j) = 0) ∧ weierstrassPolynomial d₁ c₁ * weierstrassPolynomial d₂ c₂ = weierstrassPolynomial (d₁ + d₂) c

The product of two Weierstrass polynomials is a Weierstrass polynomial of degree the sum (its residue is X^{d₁} X^{d₂}).