Adic completion

TheoremFinite free modules over adically complete rings are complete#βœ“fully proved

If π“ž is adically complete at (p) and R is finite free over π“ž, then R is adically complete at (p).

theorem IsAdicComplete.of_module_finite_free_span_natCast
    {π“ž : Type u} [CommRing π“ž] (p : β„•) [IsAdicComplete (Ideal.span {(p : π“ž)}) π“ž]
    (R : Type v) [CommRing R] [Algebra π“ž R] [Module.Finite π“ž R] [Module.Free π“ž R] :
    IsAdicComplete (Ideal.span {(p : R)}) R

TheoremAdic completion preserves Krull dimension at least two#βœ“fully proved

A Noetherian local ring of Krull dimension at least two has an adic completion of Krull dimension at least two.

theorem IsLocalRing.two_le_ringKrullDim_adicCompletion_of_two_le
    (R : Type*) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    (h : 2 ≀ ringKrullDim R) :
    2 ≀ ringKrullDim (AdicCompletion (IsLocalRing.maximalIdeal R) R)
Uses 1
Proof usesCompletion of a Noetherian local ring is faithfully flat

TheoremFinite local extensions of adically complete rings are complete#βœ“fully proved

A finite local extension of an adically complete local ring is adically complete at its maximal ideal.

theorem isAdicComplete_of_module_finite {π’ͺ : Type u} {T : Type v} [CommRing π’ͺ]
    [IsNoetherianRing π’ͺ] [IsLocalRing π’ͺ] [IsAdicComplete (IsLocalRing.maximalIdeal π’ͺ) π’ͺ]
    [CommRing T] [Algebra π’ͺ T] [Module.Finite π’ͺ T] [IsLocalRing T] :
    IsAdicComplete (IsLocalRing.maximalIdeal T) T

TheoremAdic completeness at a nilpotent ideal#βœ“fully proved

A ring is adically complete at a nilpotent ideal.

theorem IsAdicComplete.of_isNilpotent {R : Type u} [CommRing R] {I : Ideal R}
    (hI : IsNilpotent I) : IsAdicComplete I R

TheoremAdic completion of a Noetherian ring is Noetherian#βœ“fully proved

The adic completion of a Noetherian ring is Noetherian.

theorem AdicCompletion.isNoetherianRing_of_isNoetherianRing {R : Type u} [CommRing R]
    [IsNoetherianRing R] (I : Ideal R) : IsNoetherianRing (AdicCompletion I R)

TheoremAdic completeness of multivariate power series#βœ“fully proved

If R is adically complete at its maximal ideal, then MvPowerSeries Οƒ R is adically complete at its maximal ideal.

theorem isAdicComplete_maximalIdeal {Οƒ : Type u} {R : Type v} [Finite Οƒ] [CommRing R]
    [IsLocalRing R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] :
    IsAdicComplete (IsLocalRing.maximalIdeal (MvPowerSeries Οƒ R)) (MvPowerSeries Οƒ R)
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.