Power series over a regular local ring

Theorem\(X\) is a regular element of the power series ring#✓fully proved

X is a regular element of the power series ring.

theorem isSMulRegular_X : IsSMulRegular R⟦X⟧ (X : R⟦X⟧)

Used by 1

Used byKrull dimension of a power series ring

TheoremKernel of the constant coefficient map of power series#✓fully proved

The kernel of the constant coefficient map is the span of X.

theorem ker_constantCoeff : RingHom.ker (constantCoeff (R := R)) = Ideal.span {(X : R⟦X⟧)}

Used by 2

Used byGenerators of the maximal ideal of a power series ring · Power series modulo \(X\) recover the coefficient ring

DefinitionPower series modulo \(X\) recover the coefficient ring#✓fully proved

Quotienting R⟦X⟧ by the span of X recovers R.

noncomputable def quotSpanXEquiv : (R⟦X⟧ ⧸ Ideal.span {(X : R⟦X⟧)}) ≃+* R :=
  (Ideal.quotEquivOfEq ker_constantCoeff.symm).trans
    (RingHom.quotientKerEquivOfSurjective constantCoeff_surj)

Uses 1 · Used by 1

Statement usesKernel of the constant coefficient map of power series

Used byKrull dimension of a power series ring

TheoremKrull dimension of a power series ring#✓fully proved

The Krull dimension of R⟦X⟧ is one more than that of R.

theorem PowerSeries.ringKrullDim_powerSeries :
    ringKrullDim R⟦X⟧ = ringKrullDim R + 1

Uses 2 · Used by 1

Proof uses\(X\) is a regular element of the power series ring · Power series modulo \(X\) recover the coefficient ring

Used byPower series over a regular local ring are regular local

TheoremGenerators of the maximal ideal of a power series ring#✓fully proved

The maximal ideal of R⟦X⟧ is generated by the image of a generating set of the maximal ideal of R together with X.

theorem PowerSeries.maximalIdeal_eq_span_image_union_X {S : Set R}
    (hS : maximalIdeal R = Ideal.span S) :
    maximalIdeal R⟦X⟧ = Ideal.span ((C : R →+* R⟦X⟧) '' S ∪ {(X : R⟦X⟧)})

Uses 1 · Used by 1

Proof usesKernel of the constant coefficient map of power series

Used byEmbedding dimension of a power series ring

TheoremEmbedding dimension of a power series ring#✓fully proved

The embedding dimension of R⟦X⟧ is at most one more than that of R.

theorem PowerSeries.spanFinrank_maximalIdeal_le_succ [IsNoetherianRing R] :
    (maximalIdeal R⟦X⟧).spanFinrank ≤ (maximalIdeal R).spanFinrank + 1

Uses 1 · Used by 1

Proof usesGenerators of the maximal ideal of a power series ring

Used byPower series over a regular local ring are regular local

TheoremPower series over a regular local ring are regular local#✓fully proved

Power series over a regular local ring are regular local.

theorem PowerSeries.isRegularLocalRing_powerSeries (R : Type*) [CommRing R]
    [IsRegularLocalRing R] : IsRegularLocalRing R⟦X⟧

Uses 2 · Used by 1

Proof usesKrull dimension of a power series ring · Embedding dimension of a power series ring

Used byMultivariable power series over a regular local ring are regular local

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.