Basic Properties of Complete Local Ring

In this file we prove that for local ring R with finitely generated maximal ideal, AdicCompletion (IsLocalRing.maximalIdeal R) R is local ring with maximal ideal equal to IsLocalRing.maximalIdeal R mapped by algebra map. Furthermore, it is complete with respect to its maximal ideal.

As a corollary, for Noetherian local ring R, AdicCompletion (maximalIdeal R) R is always a complete Noetherian local ring.

Most results needing finitely generation of maximal ideal have a version for Noetherian ring without this side condition for convenience.

Main Results

• AdicCompletion.isLocalRing_of_fg : for a local ring R with finitely generated maximal ideal, its completion with respect to IsLocalRing.maximalIdeal R is local ring.

• AdicCompletion.maximalIdeal_eq_map_of_fg : for a local ring R with finitely generated maximal ideal, the maximal ideal of its completion with respect to IsLocalRing.maximalIdeal R is equal to IsLocalRing.maximalIdeal R mapped by algebra map.

• AdicCompletion.isAdicComplete_of_fg : for a local ring R with finitely generated maximal ideal, AdicCompletion (IsLocalRing.maximalIdeal R) R itself is complete with respect to its maximal ideal.

• AdicCompletion.spanFinrank_maximalIdeal_eq : for Noetherian local ring R, minimal number of generators of maximal ideal of R and AdicCompletion (IsLocalRing.maximalIdeal R) R are equal.

theorem isLocalRing_of_isAdicComplete_maximal {R : Type u_1} [CommRing R] (m : Ideal R) [m.IsMaximal] [IsAdicComplete m R] : IsLocalRing R

theorem AdicCompletion.isAdicComplete_self {R : Type u_1} [CommRing R] (I : Ideal R) (fg : I.FG) : IsAdicComplete (Ideal.map (algebraMap R (AdicCompletion I R)) I) (AdicCompletion I R)

theorem AdicCompletion.isMaximal_map_of_le {R : Type u_1} [CommRing R] (I m : Ideal R) [m.IsMaximal] (le : I ≤ m) (fg : I.FG) : (Ideal.map (algebraMap R (AdicCompletion I R)) m).IsMaximal

theorem AdicCompletion.isLocalRing_of_fg {R : Type u_1} [CommRing R] [IsLocalRing R] (fg : (IsLocalRing.maximalIdeal R).FG) : IsLocalRing (AdicCompletion (IsLocalRing.maximalIdeal R) R)

instance AdicCompletion.instIsLocalRingMaximalIdealOfIsNoetherianRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : IsLocalRing (AdicCompletion (IsLocalRing.maximalIdeal R) R)

theorem AdicCompletion.maximalIdeal_eq_map_of_fg {R : Type u_1} [CommRing R] [IsLocalRing R] (fg : (IsLocalRing.maximalIdeal R).FG) : IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R) = Ideal.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.maximalIdeal R)

theorem AdicCompletion.maximalIdeal_eq_map {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R) = Ideal.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.maximalIdeal R)

theorem AdicCompletion.mem_maximalIdeal_iff_eval_one_eq_zero {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (x : AdicCompletion (IsLocalRing.maximalIdeal R) R) : x ∈ IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R) ↔ ↑x 1 = 0

theorem AdicCompletion.algebraMap_isLocalHom_of_fg {R : Type u_1} [CommRing R] [IsLocalRing R] (fg : (IsLocalRing.maximalIdeal R).FG) : IsLocalHom (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R))

instance AdicCompletion.instIsLocalHomMaximalIdealRingHomAlgebraMapOfIsNoetherianRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : IsLocalHom (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R))

theorem AdicCompletion.isAdicComplete_of_fg {R : Type u_1} [CommRing R] [IsLocalRing R] (fg : (IsLocalRing.maximalIdeal R).FG) : IsAdicComplete (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (AdicCompletion (IsLocalRing.maximalIdeal R) R)

instance AdicCompletion.instIsAdicCompleteMaximalIdeal {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : IsAdicComplete (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (AdicCompletion (IsLocalRing.maximalIdeal R) R)

theorem AdicCompletion.residueField_map_bijective_of_fg {R : Type u_1} [CommRing R] [IsLocalRing R] (fg : (IsLocalRing.maximalIdeal R).FG) : Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)))

theorem AdicCompletion.residueField_map_bijective (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)))

theorem AdicCompletion.spanFinrank_maximalIdeal_eq {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : Submodule.spanFinrank (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R)) = Submodule.spanFinrank (IsLocalRing.maximalIdeal R)