Adic Completion of a Noetherian Local Ring is Local

The M-adic completion of a Noetherian local ring (R, M) is again a local ring. The maximal ideal of the completion is the kernel of the natural surjection onto the residue field R/M.

Transition compatibility for evalₐ

theorem AdicCompletion.factorPow_comp_evalₐ {R : Type u_1} [CommRing R] (I : Ideal R) {m n : ℕ} (hmn : m ≤ n) (x : AdicCompletion I R) : (Ideal.Quotient.factorPow I hmn) ((evalₐ I n) x) = (evalₐ I m) x

The transition ring hom factorPow is compatible with evalₐ: factorPow I hmn (evalₐ I n x) = evalₐ I m x.

Constructing inverses from componentwise units

theorem AdicCompletion.evalₐ_isUnit_of_evalOneₐ_isUnit {R : Type u_1} [CommRing R] (I : Ideal R) (x : AdicCompletion I R) (hu : IsUnit ((evalOneₐ I) x)) (n : ℕ) : IsUnit ((evalₐ I n) x)

If evalOneₐ I x is a unit (in the residue field R ⧸ I), then evalₐ I n x is a unit in R ⧸ I ^ n for every n.

noncomputable def AdicCompletion.mkInverse {R : Type u_1} [CommRing R] (I : Ideal R) (x : AdicCompletion I R) (hu : ∀ (n : ℕ), IsUnit ((evalₐ I n) x)) : AdicCompletion I R

Given x with all evalₐ components invertible, construct the inverse as an element of AdicCompletion.

Equations

• AdicCompletion.mkInverse I x hu = ⟨fun (n : ℕ) => (Ideal.quotientEquivAlgOfEq R ⋯).symm ↑⋯.unit⁻¹, ⋯⟩

theorem AdicCompletion.evalₐ_mkInverse {R : Type u_1} [CommRing R] (I : Ideal R) (x : AdicCompletion I R) (hu : ∀ (n : ℕ), IsUnit ((evalₐ I n) x)) (n : ℕ) : (evalₐ I n) (mkInverse I x hu) = ↑⋯.unit⁻¹

theorem AdicCompletion.mkInverse_mul {R : Type u_1} [CommRing R] (I : Ideal R) (x : AdicCompletion I R) (hu : ∀ (n : ℕ), IsUnit ((evalₐ I n) x)) : mkInverse I x hu * x = 1

theorem AdicCompletion.isUnit_of_evalOneₐ_isUnit {R : Type u_1} [CommRing R] (I : Ideal R) (x : AdicCompletion I R) (hu : IsUnit ((evalOneₐ I) x)) : IsUnit x

An element of the adic completion whose image under evalOneₐ is a unit (in the residue field) is itself a unit.

Main theorem

@[reducible, inline]

abbrev AdicCompletion.M' (R : Type u_2) [CommRing R] [IsLocalRing R] : Ideal R

Local abbreviation for the maximal ideal IsLocalRing.maximalIdeal R.

Equations

• AdicCompletion.M' R = IsLocalRing.maximalIdeal R

instance AdicCompletion.adicCompletion_nontrivial (R : Type u_2) [CommRing R] [IsLocalRing R] : Nontrivial (AdicCompletion (M' R) R)

theorem AdicCompletion.field_isUnit_or_isUnit {K : Type u_3} [Field K] {a b : K} (hab : a + b = 1) : IsUnit a ∨ IsUnit b

theorem AdicCompletion.adicCompletion_isLocalRing (R : Type u_2) [CommRing R] [IsLocalRing R] : IsLocalRing (AdicCompletion (M' R) R)

theorem adicCompletion_isLocalRing (R : Type u_2) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : IsLocalRing (AdicCompletion (IsLocalRing.maximalIdeal R) R)