The ring Conv K m: domain, local ring, the tail embedding and polynomial evaluation

The definitions and instances that Rückert's theorems on the ring of convergent power series (Noetherianity, unique factorization, the Nullstellensatz) use throughout, in the classical setting of [GR65, Chapter II, §B]:

• Conv K m is a domain (instIsDomainConv): orders add (order_mul), so a product of nonzero series is nonzero; and a local ring (instIsLocalRingConv): the units are the series with nonzero constant coefficient (isUnit_iff_constantCoeff_ne_zero), whose complement is closed under addition. This is the local ring 𝒪_a of germs of [BM88, p. 23].
• convTail : Conv K m →ₐ[K] Conv K (m+1), the embedding of the tail series (liftTail). No global Algebra (Conv K m) (Conv K (m+1)) instance is declared (instance search for SMul (Conv K m) (Conv K (m+1)) through the subalgebra coercions does not terminate in reasonable time); module structures over Conv K m are introduced locally where the Noetherian argument needs them.
• convPolyEval : (Conv K m)[X] →+* Conv K (m+1), evaluation at x_0 with coefficients embedded by convTail (Polynomial.eval₂RingHom), sending weierstrassPolynomial d c to the series weierstrassPoly d c.

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

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

Conv K m has no zero divisors: orders add.

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

Conv K m is a domain.

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

Conv K m is a local ring: the nonunits are the series vanishing at 0, closed under addition [GR65, Chapter II, §B].

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

The tail embedding Conv K m → Conv K (m+1) (the series in x_1, …, x_m as series in all variables, liftTail), as a K-algebra map.

Equations

• Analytic.convTail K = ((MvPowerSeries.rename Fin.succ).comp (Analytic.Conv K m).val).codRestrict (Analytic.Conv K (m + 1)) ⋯

@[simp]

theorem Analytic.coe_convTail {K : Type u_1} [RCLike K] {m : ℕ} (c : ↥(Conv K m)) : ↑((convTail K) c) = liftTail ↑c

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

Evaluation of a polynomial over Conv K m at x_0, as a ring map (Conv K m)[X] → Conv K (m+1) (coefficients embedded by convTail).

Equations

• Analytic.convPolyEval K = Polynomial.eval₂RingHom (Analytic.convTail K).toRingHom (Analytic.convX K 0)

@[simp]

theorem Analytic.convPolyEval_C {K : Type u_1} [RCLike K] {m : ℕ} (c : ↥(Conv K m)) : (convPolyEval K) (Polynomial.C c) = (convTail K) c

@[simp]

theorem Analytic.convPolyEval_X (K : Type u_1) [RCLike K] {m : ℕ} : (convPolyEval K) Polynomial.X = convX K 0