The formal power series ring is complete for its maximal ideal

Mathlib's formal Weierstrass division and preparation (PowerSeries.exists_isWeierstrassDivision, PowerSeries.exists_isWeierstrassFactorization) are stated over a coefficient ring A with IsAdicComplete (maximalIdeal A) A. This module supplies that instance for the tail ring A = MvPowerSeries (Fin m) K.

The maximal ideal 𝔪 consists of the series with zero constant term, and f ∈ 𝔪^n iff every coefficient of f of total degree < n vanishes: one direction by induction on the product structure of 𝔪^n (Submodule.pow_induction_on_left'), the other by writing a series without constant term as ∑_i x_i · D_i f, where D_i f collects the monomials whose least variable is x_i, and inducting on n. Hausdorffness (⋂ 𝔪^n = 0) and precompleteness (a coherent sequence f_n mod 𝔪^n has the limit whose ν-coefficient is that of f_{|ν|+1}) are then read off coefficientwise. Not in the sources, which quote the formal Weierstrass theorems as classical.

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

theorem Analytic.mem_maximalIdeal_iff {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin m) K) : f ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K) ↔ MvPowerSeries.constantCoeff f = 0

The maximal ideal of the formal power series ring: zero constant term.

theorem Analytic.X_mem_maximalIdeal {K : Type u_1} [RCLike K] {m : ℕ} (i : Fin m) : MvPowerSeries.X i ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K)

theorem Analytic.coeff_eq_zero_of_mem_maximalIdeal_pow {K : Type u_1} [RCLike K] {m n : ℕ} {f : MvPowerSeries (Fin m) K} (hf : f ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K) ^ n) (d : Fin m →₀ ℕ) (hd : Finsupp.degree d < n) : (MvPowerSeries.coeff d) f = 0

Elements of 𝔪^n have no coefficients of total degree < n.

noncomputable def Analytic.leastVarShift {K : Type u_1} [RCLike K] {m : ℕ} (i : Fin m) (f : MvPowerSeries (Fin m) K) : MvPowerSeries (Fin m) K

The monomials of f whose least variable is x_i, divided by x_i.

Equations

• Analytic.leastVarShift i f ν = if ∀ j < i, ν j = 0 then (MvPowerSeries.coeff (ν + Finsupp.single i 1)) f else 0

theorem Analytic.coeff_leastVarShift {K : Type u_1} [RCLike K] {m : ℕ} (i : Fin m) (f : MvPowerSeries (Fin m) K) (ν : Fin m →₀ ℕ) : (MvPowerSeries.coeff ν) (leastVarShift i f) = if ∀ j < i, ν j = 0 then (MvPowerSeries.coeff (ν + Finsupp.single i 1)) f else 0

theorem Analytic.sum_X_mul_leastVarShift {K : Type u_1} [RCLike K] {m : ℕ} {f : MvPowerSeries (Fin m) K} (hf : MvPowerSeries.constantCoeff f = 0) : ∑ i : Fin m, MvPowerSeries.X i * leastVarShift i f = f

A series without constant term is ∑_i x_i · D_i f, grouping each monomial under its least variable.

theorem Analytic.mem_maximalIdeal_pow_of_coeff {K : Type u_1} [RCLike K] {m : ℕ} (n : ℕ) {f : MvPowerSeries (Fin m) K} (hf : ∀ (d : Fin m →₀ ℕ), Finsupp.degree d < n → (MvPowerSeries.coeff d) f = 0) : f ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K) ^ n

A series with no coefficients of total degree < n lies in 𝔪^n.

theorem Analytic.mem_maximalIdeal_pow_iff {K : Type u_1} [RCLike K] {m : ℕ} (n : ℕ) (f : MvPowerSeries (Fin m) K) : f ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K) ^ n ↔ ∀ (d : Fin m →₀ ℕ), Finsupp.degree d < n → (MvPowerSeries.coeff d) f = 0

The coefficientwise description of 𝔪^n: no coefficients of total degree < n.

theorem Analytic.maximalIdeal_pow_smul_top {K : Type u_1} [RCLike K] {m : ℕ} (n : ℕ) : IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K) ^ n • ⊤ = IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K) ^ n

instance Analytic.isHausdorff_maximalIdeal {K : Type u_1} [RCLike K] {m : ℕ} : IsHausdorff (IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K)) (MvPowerSeries (Fin m) K)

⋂_n 𝔪^n = 0: the topology of the maximal ideal is Hausdorff.

noncomputable def Analytic.adicLimit {K : Type u_1} [RCLike K] {m : ℕ} (f : ℕ → MvPowerSeries (Fin m) K) : MvPowerSeries (Fin m) K

The limit of a sequence coherent modulo the powers of 𝔪: the ν-coefficient of the (|ν| + 1)-st term.

Equations

• Analytic.adicLimit f d = (MvPowerSeries.coeff d) (f (Finsupp.degree d + 1))

theorem Analytic.coeff_adicLimit {K : Type u_1} [RCLike K] {m : ℕ} (f : ℕ → MvPowerSeries (Fin m) K) (d : Fin m →₀ ℕ) : (MvPowerSeries.coeff d) (adicLimit f) = (MvPowerSeries.coeff d) (f (Finsupp.degree d + 1))

instance Analytic.isPrecomplete_maximalIdeal {K : Type u_1} [RCLike K] {m : ℕ} : IsPrecomplete (IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K)) (MvPowerSeries (Fin m) K)

A sequence coherent modulo 𝔪^n has a limit; its ν-coefficient is the ν-coefficient of the (|ν| + 1)-st term.

instance Analytic.isAdicComplete_maximalIdeal (K : Type u_1) [RCLike K] (m : ℕ) : IsAdicComplete (IsLocalRing.maximalIdeal (MvPowerSeries (Fin m) K)) (MvPowerSeries (Fin m) K)

MvPowerSeries (Fin m) K is complete for its maximal ideal, the hypothesis of Mathlib's formal Weierstrass theorems.