K⟦X₁, …, Xₙ⟧ is a regular local ring of dimension n

Kollár identifies the completion of a smooth stalk with k(p)⟦x₁, …, xₙ⟧ [Kol07, Definition 55]; the library needs the target to be a regular local ring of dimension n, a fact Mathlib does not state.

The argument. Two bounds meet:

• spanFinrank 𝔪 ≤ n, because 𝔪 = ⟨X₁, …, Xₙ⟧ (MvPowerSeries.maximalIdeal_eq_span_range_X) is spanned by the n variables (Submodule.spanFinrank_span_le_ncard_of_finite);
• n ≤ dim K⟦X₁, …, Xₙ⟧, by induction on n through K⟦X₁, …, X_{n+1}⟧ ≅ K⟦X₁, …, Xₙ⟧⟦X⟧ (MvPowerSeries.finSuccEquiv) and dim R + 1 ≤ dim R⟦X⟧ (ringKrullDim_succ_le_ringKrullDim_powerseries: X is a nonzerodivisor with R⟦X⟧/(X) ≅ R).

Since K⟦X⟧ is Noetherian (MvPowerSeries.isNoetherianRing) and local, Krull's height theorem gives dim ≤ spanFinrank 𝔪 for free (ringKrullDim_le_spanFinrank_maximalIdeal), so spanFinrank 𝔪 ≤ n ≤ dim ≤ spanFinrank 𝔪: the ring is regular (IsRegularLocalRing.of_spanFinrank_maximalIdeal_le) of dimension exactly n. No chain of primes needs to be exhibited, and no characteristic hypothesis enters.

theorem IsLocalRing.natCast_le_ringKrullDim_mvPowerSeries (K : Type u_1) [Field K] (n : ℕ) : ↑n ≤ ringKrullDim (MvPowerSeries (Fin n) K)

n ≤ dim K⟦X₁, …, Xₙ⟧, by induction through K⟦X₁, …, X_{n+1}⟧ ≅ K⟦X₁, …, Xₙ⟧⟦X⟧ and dim R + 1 ≤ dim R⟦X⟧.

theorem IsLocalRing.spanFinrank_maximalIdeal_mvPowerSeries_le (K : Type u_1) [Field K] (n : ℕ) : Submodule.spanFinrank (maximalIdeal (MvPowerSeries (Fin n) K)) ≤ n

𝔪 = ⟨X₁, …, Xₙ⟧ needs at most n generators.

theorem IsLocalRing.isRegularLocalRing_mvPowerSeries (K : Type u_1) [Field K] (n : ℕ) : IsRegularLocalRing (MvPowerSeries (Fin n) K)

K⟦X₁, …, Xₙ⟧ is a regular local ring (the target of the identification of [Kol07, Definition 55]).

instance IsLocalRing.instIsRegularLocalRingMvPowerSeries (K : Type u_1) [Field K] (n : ℕ) : IsRegularLocalRing (MvPowerSeries (Fin n) K)

The regularity of K⟦X₁, …, Xₙ⟧ as an instance, so that constructions such as RegularCoords.mvPowerSeries find it by instance search.

theorem IsLocalRing.ringKrullDim_mvPowerSeries (K : Type u_1) [Field K] (n : ℕ) : ringKrullDim (MvPowerSeries (Fin n) K) = ↑n

dim K⟦X₁, …, Xₙ⟧ = n.

@[reducible, inline]

noncomputable abbrev IsLocalRing.RegularCoords.stdMvPowerSeries (K : Type u_1) [Field K] [CharZero K] (n : ℕ) : RegularCoords (MvPowerSeries (Fin n) K) n

The coordinate structure RegularCoords.mvPowerSeries on K⟦X₁, …, Xₙ⟧ with its hypotheses discharged.

Equations

• IsLocalRing.RegularCoords.stdMvPowerSeries K n = IsLocalRing.RegularCoords.mvPowerSeries K n ⋯ ⋯