Power series over a regular local ring

Let (R, 𝔪) be a Noetherian local ring. The ring of formal power series R⟦X⟧ is again a Noetherian local ring, whose maximal ideal is the preimage of 𝔪 under the constant coefficient, generated by X together with generators of 𝔪. This file computes its Krull dimension,

dim R⟦X⟧ = dim R + 1,

and deduces that R⟦X⟧ is regular whenever R is: a regular system of parameters of R together with X is one of R⟦X⟧.

The case of a discrete valuation ring O with uniformizer ϖ is the Iwasawa algebra Λ = O⟦T⟧: it is a regular local ring of dimension two, with maximal ideal (ϖ, T). This is the ring-theoretic starting point of the structure theory of finitely generated Λ-modules. No completeness of O and no finiteness of its residue field is needed for this.

Main results

• TauCeti.PowerSeries.maximalIdeal_eq_comap_constantCoeff: the maximal ideal of R⟦X⟧ consists of the series whose constant coefficient lies in 𝔪.
• TauCeti.PowerSeries.maximalIdeal_eq_span_insert_X: generators of 𝔪 together with X generate the maximal ideal of R⟦X⟧.
• TauCeti.PowerSeries.ringKrullDim_of_isNoetherianRing_of_isLocalRing: for a Noetherian local ring R, dim R⟦X⟧ = dim R + 1.
• TauCeti.PowerSeries.isRegularLocalRing: power series over a regular local ring form a regular local ring.
• TauCeti.PowerSeries.ringKrullDim_of_isDiscreteValuationRing and TauCeti.PowerSeries.maximalIdeal_eq_span_C_X: over a discrete valuation ring with uniformizer ϖ, the power series ring has dimension two and maximal ideal (ϖ, X).

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Springer (2008), (5.3.6).
• H. Matsumura, Commutative Ring Theory, §14 and §15.
• The generation of ideals of R⟦X⟧ from their constant coefficients, used for the maximal ideal and its generators here, is Mathlib's Mathlib.RingTheory.PowerSeries.Ideal, by Riccardo Brasca, Anthony Fernandes and Marc Robin.

theorem TauCeti.PowerSeries.ker_constantCoeff {R : Type u_1} [CommRing R] : RingHom.ker PowerSeries.constantCoeff = Ideal.span {PowerSeries.X}

The kernel of the constant coefficient map on R⟦X⟧ is the ideal generated by X.

instance TauCeti.PowerSeries.isLocalHom_constantCoeff {R : Type u_1} [CommRing R] : IsLocalHom PowerSeries.constantCoeff

The constant coefficient is a local homomorphism: a power series is a unit exactly when its constant coefficient is.

theorem TauCeti.PowerSeries.maximalIdeal_eq_comap_constantCoeff {R : Type u_1} [CommRing R] [IsLocalRing R] : IsLocalRing.maximalIdeal (PowerSeries R) = Ideal.comap PowerSeries.constantCoeff (IsLocalRing.maximalIdeal R)

The maximal ideal of R⟦X⟧ over a local ring R consists of the series whose constant coefficient lies in the maximal ideal of R.

theorem TauCeti.PowerSeries.X_mem_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] : PowerSeries.X ∈ IsLocalRing.maximalIdeal (PowerSeries R)

Over a local ring, the variable lies in the maximal ideal of the power series ring.

@[simp]

theorem TauCeti.PowerSeries.map_constantCoeff_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] : Ideal.map PowerSeries.constantCoeff (IsLocalRing.maximalIdeal (PowerSeries R)) = IsLocalRing.maximalIdeal R

The constant coefficients of the series in the maximal ideal of R⟦X⟧ form the maximal ideal of R.

theorem TauCeti.PowerSeries.maximalIdeal_eq_span_insert_X {R : Type u_1} [CommRing R] [IsLocalRing R] {S : Set R} (hS : Ideal.span S = IsLocalRing.maximalIdeal R) : IsLocalRing.maximalIdeal (PowerSeries R) = Ideal.span (insert PowerSeries.X (⇑PowerSeries.C '' S))

If S generates the maximal ideal of a local ring R, then X together with the constant series C s, s ∈ S, generate the maximal ideal of R⟦X⟧.

theorem TauCeti.PowerSeries.spanFinrank_maximalIdeal_le {R : Type u_1} [CommRing R] [IsLocalRing R] : Submodule.spanFinrank (IsLocalRing.maximalIdeal (PowerSeries R)) ≤ Submodule.spanFinrank (IsLocalRing.maximalIdeal R) + 1

The maximal ideal of R⟦X⟧ needs at most one generator more than that of R.

theorem TauCeti.PowerSeries.bijective_residueFieldMap_constantCoeff {R : Type u_1} [CommRing R] [IsLocalRing R] : Function.Bijective ⇑(IsLocalRing.ResidueField.map PowerSeries.constantCoeff)

The constant coefficient induces a bijection of residue fields.

noncomputable def TauCeti.PowerSeries.residueFieldEquiv {R : Type u_1} [CommRing R] [IsLocalRing R] : IsLocalRing.ResidueField (PowerSeries R) ≃+* IsLocalRing.ResidueField R

The residue field of R⟦X⟧ is the residue field of R, through the constant coefficient.

@[simp]

theorem PowerSeries.residueFieldEquiv_residue {R : Type u_1} [CommRing R] [IsLocalRing R] (f : PowerSeries R) : TauCeti.PowerSeries.residueFieldEquiv ((IsLocalRing.residue (PowerSeries R)) f) = (IsLocalRing.residue R) (constantCoeff f)

The residue field equivalence takes the residue class of f to that of its constant coefficient.

@[simp]

theorem TauCeti.PowerSeries.residueFieldEquiv_symm_residue {R : Type u_1} [CommRing R] [IsLocalRing R] (r : R) : residueFieldEquiv.symm ((IsLocalRing.residue R) r) = (IsLocalRing.residue (PowerSeries R)) (PowerSeries.C r)

The inverse of the residue field equivalence takes the residue class of r to that of the constant series C r.

instance TauCeti.PowerSeries.instFiniteResidueFieldPowerSeries_tauCeti {R : Type u_1} [CommRing R] [IsLocalRing R] [Finite (IsLocalRing.ResidueField R)] : Finite (IsLocalRing.ResidueField (PowerSeries R))

A finite residue field passes to the power series ring.

theorem TauCeti.PowerSeries.ringKrullDim_of_isNoetherianRing_of_isLocalRing {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : ringKrullDim (PowerSeries R) = ringKrullDim R + 1

The dimension of a power series ring. Over a Noetherian local ring R, adjoining a formal power series variable raises the Krull dimension by exactly one.

instance TauCeti.PowerSeries.isRegularLocalRing {R : Type u_1} [CommRing R] [IsRegularLocalRing R] : IsRegularLocalRing (PowerSeries R)

Power series over a regular local ring form a regular local ring. A regular system of parameters of R together with X is one of R⟦X⟧ (maximalIdeal_eq_span_insert_X).

theorem TauCeti.PowerSeries.ringKrullDim_of_isDiscreteValuationRing {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : ringKrullDim (PowerSeries R) = 2

The power series ring over a discrete valuation ring has Krull dimension two. It is a regular local ring by isRegularLocalRing.

theorem TauCeti.PowerSeries.maximalIdeal_eq_span_C_X {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} (hϖ : Irreducible ϖ) : IsLocalRing.maximalIdeal (PowerSeries R) = Ideal.span {PowerSeries.C ϖ, PowerSeries.X}

Over a discrete valuation ring with uniformizer ϖ, the maximal ideal of the power series ring is (ϖ, X); these two elements form a regular system of parameters.