Irreducible Weierstrass polynomials stay irreducible in Conv K (m+1)

Let W ∈ (Conv K m)[X] be a Weierstrass polynomial, irreducible there, and P = W(x_0) ∈ Conv K (m+1). P is not a unit (P(0) = 0 since d ≥ 1). If P = a b, then a and b are x_0-regular of orders d₁ + d₂ = d (the axis restriction is multiplicative, axis_mul, and orders add: isRegularIn_of_mul); the convergent Weierstrass preparation writes a = u₁ W₁(x_0), b = u₂ W₂(x_0) with Weierstrass polynomials W₁, W₂ (exists_preparation_conv), so P = (u₁ u₂) (W₁ W₂)(x_0) with W₁ W₂ Weierstrass (exists_weierstrassPolynomial_mul); the uniqueness clause of the preparation (preparation_unique) gives W = W₁ W₂, and irreducibility of W forces W₁ = 1 or W₂ = 1, i.e. a or b is a unit. This is a standard step of the theory of the ring of convergent series [GR65, Chapter II, §B]; UFD.lean uses the preparation lemmas of this module.

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

theorem Analytic.isRegularIn_iff_order_axis {K : Type u_1} [RCLike K] {m : ℕ} (g : MvPowerSeries (Fin (m + 1)) K) (d : ℕ) : IsRegularIn g d ↔ (axis g).order = ↑d

x_0-regularity of order d is the order of the axis restriction axis: the printed f_a(0, …, 0, x_m) ∼ x_m^e of [BM88, proof of Theorem 4.4, p. 24].

theorem Analytic.isRegularIn_of_mul {K : Type u_1} [RCLike K] {m : ℕ} {a b : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} (h : IsRegularIn (a * b) d) : ∃ (d₁ : ℕ) (d₂ : ℕ), d₁ + d₂ = d ∧ IsRegularIn a d₁ ∧ IsRegularIn b d₂

The factors of an x_0-regular series are x_0-regular, with orders adding up (axis_mul and order_mul).

theorem Analytic.exists_preparation_conv {K : Type u_1} [RCLike K] {m : ℕ} {g : ↥(Conv K (m + 1))} {d : ℕ} (hreg : IsRegularIn (↑g) d) : ∃ (u : ↥(Conv K (m + 1))) (c : Fin d → ↥(Conv K m)), IsUnit u ∧ (∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) ∧ g = u * (convPolyEval K) (weierstrassPolynomial d c)

The convergent Weierstrass preparation for elements of Conv K (m+1): a regular g is a unit times the evaluation of a Weierstrass polynomial over Conv K m.

theorem Analytic.preparation_unique {K : Type u_1} [RCLike K] {m : ℕ} {g : ↥(Conv K (m + 1))} {d : ℕ} (hreg : IsRegularIn (↑g) d) {u u' : ↥(Conv K (m + 1))} {c c' : Fin d → ↥(Conv K m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) (hc' : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c' j) = 0) (h : g = u * (convPolyEval K) (weierstrassPolynomial d c)) (h' : g = u' * (convPolyEval K) (weierstrassPolynomial d c')) : u = u' ∧ c = c'

Uniqueness of the preparation in Conv K (m+1).

theorem Analytic.irreducible_convPolyEval_of_irreducible {K : Type u_1} [RCLike K] {m d : ℕ} {c : Fin d → ↥(Conv K m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) (hirr : Irreducible (weierstrassPolynomial d c)) : Irreducible ((convPolyEval K) (weierstrassPolynomial d c))

A Weierstrass polynomial irreducible in (Conv K m)[X] is irreducible in Conv K (m+1) [GR65, Chapter II, §B]: regularity of the factors, preparation, uniqueness of preparation.