Conv K m is a unique factorization domain

The ring of convergent power series is a unique factorization domain [GR65, Chapter II, §B], [Nar66, Chapter II]. Induction on m. Conv K 0 ≅ K is a field. For m + 1, by UniqueFactorizationMonoid.of_exists_prime_factors it suffices to factor every nonzero a into primes up to a unit. A unit is the empty product. A nonunit becomes, after a linear change of variables (substEquiv, Subst.lean), regular of order d ≥ 1, hence u · W(x_0) with W a Weierstrass polynomial over Conv K m (the preparation theorem). W(x_0) is a product of primes of Conv K (m+1) by strong induction on d (exists_prime_factors_convPolyEval_weierstrass): if W is irreducible in (Conv K m)[X], it is prime there (Gauss's lemma and the induction hypothesis on m), so Conv K (m+1) ⧸ (W(x_0)) ≃ (Conv K m)[X] ⧸ (W) (Quotient.lean) is a domain and W(x_0) is prime; otherwise W = a' b' with a', b' monic nonunits (normalizing the leading coefficients, which are units since their product is 1), both Weierstrass by MonicDivisor.lean and of smaller degree. Transporting back along the automorphism gives the factorization of a (primes are preserved by ring isomorphisms). The route by strong induction on the degree replaces the direct appeal to the factorization in (Conv K m)[X] of the textbooks.

Mathlib has UniqueFactorizationMonoid (PowerSeries k) in one variable only; nothing for MvPowerSeries. Unique factorization gives the integral closedness of the base ring in the parametrization theorem (MinpolyDvd.lean) and the square-free reduction of the hypersurface Nullstellensatz (Hypersurface.lean).

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

theorem Analytic.uniqueFactorizationMonoid_polynomial_conv (K : Type u_1) [RCLike K] {m : ℕ} [UniqueFactorizationMonoid ↥(Conv K m)] : UniqueFactorizationMonoid (Polynomial ↥(Conv K m))

(Conv K m)[X] is a unique factorization domain when Conv K m is (Gauss's lemma, Mathlib's Polynomial.uniqueFactorizationMonoid).

theorem Analytic.uniqueFactorizationMonoid_conv_zero {K : Type u_1} [RCLike K] : UniqueFactorizationMonoid ↥(Conv K 0)

Conv K 0 is a unique factorization domain (a field).

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

A Weierstrass polynomial prime in (Conv K m)[X] evaluates to a prime of Conv K (m+1) (the quotients are isomorphic, Quotient.lean).

theorem Analytic.exists_prime_factors_convPolyEval_weierstrass {K : Type u_1} [RCLike K] {m : ℕ} [UniqueFactorizationMonoid ↥(Conv K m)] (d : ℕ) (c : Fin d → ↥(Conv K m)) : (∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) → ∃ (f : Multiset ↥(Conv K (m + 1))), (∀ b ∈ f, Prime b) ∧ f.prod = (convPolyEval K) (weierstrassPolynomial d c)

The evaluation of a Weierstrass polynomial is a product of primes of Conv K (m+1), by strong induction on the degree.

theorem Analytic.uniqueFactorizationMonoid_conv_succ {K : Type u_1} [RCLike K] {m : ℕ} [UniqueFactorizationMonoid ↥(Conv K m)] : UniqueFactorizationMonoid ↥(Conv K (m + 1))

The inductive step: if Conv K m is a unique factorization domain, so is Conv K (m+1) [GR65, Chapter II, §B].

theorem Analytic.uniqueFactorizationMonoid_conv (K : Type u_1) [RCLike K] {m : ℕ} : UniqueFactorizationMonoid ↥(Conv K m)

Conv K m is a unique factorization domain [GR65, Chapter II, §B], [Nar66, Chapter II], by induction on m.

instance Analytic.instUniqueFactorizationMonoidConv (K : Type u_1) [RCLike K] {m : ℕ} : UniqueFactorizationMonoid ↥(Conv K m)

Unique factorization as an instance (the theorem uniqueFactorizationMonoid_conv registered for instance search).