Kernel of the Evaluation Map on Adic Completions

For a Noetherian local ring (R, M) and n : N, an element of the M-adic completion that maps to zero under the canonical projection to R/M^n must lie in the n-th power of the extended maximal ideal. This uses the short exact sequence relating the completion to successive quotients.

R ⧸ I^n is I-adically complete

theorem smul_eq_zero_of_quotient {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) (x : R ⧸ I ^ n • ⊤) (hx : x ∈ I ^ n • ⊤) : x = 0

instance quotientIsHausdorff {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : IsHausdorff I (R ⧸ I ^ n • ⊤)

instance quotientIsPrecomplete {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : IsPrecomplete I (R ⧸ I ^ n • ⊤)

instance quotientAdicComplete {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : IsAdicComplete I (R ⧸ I ^ n • ⊤)

Key lemma: evalₐ I n x = 0 → x ∈ I^n • ⊤

theorem ker_evalₐ_le_smul_top {R : Type u_1} [CommRing R] (I : Ideal R) [IsNoetherianRing R] (n : ℕ) (x : AdicCompletion I R) (hx : (AdicCompletion.evalₐ I n) x = 0) : x ∈ I ^ n • ⊤

If evalₐ I n x = 0, then x ∈ I^n • ⊤ (as R-submodule of R̂). This is the backward half of ker(evalₐ I n) = (Ideal.map f I)^n.

Main theorem: kernel of evalₐ is contained in the power of the extended maximal ideal

theorem mem_map_pow_of_evalₐ_eq_zero (R : Type u_2) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (n : ℕ) (x : AdicCompletion (IsLocalRing.maximalIdeal R) R) (hx : (AdicCompletion.evalₐ (IsLocalRing.maximalIdeal R) n) x = 0) : x ∈ Ideal.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.maximalIdeal R) ^ n

If an element x of the 𝔪-adic completion of a Noetherian local ring (R, 𝔪) satisfies evalₐ 𝔪 n x = 0, then x ∈ (𝔪̂)^n where 𝔪̂ = Ideal.map (algebraMap R R̂) 𝔪.