Adic Completion of a Noetherian Local Ring is Noetherian

For a Noetherian local ring (R, M), the M-adic completion R-hat is Noetherian. The key facts are that R-hat / M-hat^n is isomorphic to R / M^n for each n, and that the completion is M-adically complete, so the Noetherian property lifts by successive approximation (Atiyah--Macdonald, Prop. 10.11).

Part 1: ker(evalₐ I n) = (map f I)ⁿ

theorem map_pow_le_ker_evalₐ {R : Type u_1} [CommRing R] (I : Ideal R) (n : ℕ) : Ideal.map (algebraMap R (AdicCompletion I R)) (I ^ n) ≤ RingHom.ker (AdicCompletion.evalₐ I n).toRingHom

theorem ker_evalₐ_eq {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (n : ℕ) : RingHom.ker (AdicCompletion.evalₐ (IsLocalRing.maximalIdeal R) n).toRingHom = Ideal.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.maximalIdeal R) ^ n

theorem eval_cauchy_stable {R : Type u_1} [CommRing R] (I : Ideal R) (f : ℕ → AdicCompletion I R) (hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) {k n : ℕ} (hkn : k ≤ n) : (AdicCompletion.evalₐ I k) (f n) = (AdicCompletion.evalₐ I k) (f k)

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

Part 2: R̂/M̂ⁿ ≅ R/Mⁿ

noncomputable def quotientPowEquiv {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (n : ℕ) : AdicCompletion (IsLocalRing.maximalIdeal R) R ⧸ Ideal.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.maximalIdeal R) ^ n ≃+* R ⧸ IsLocalRing.maximalIdeal R ^ n

R̂ / M̂ⁿ ≅ R / Mⁿ as rings.

Equations

• quotientPowEquiv n = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

Part 3: IsPrecomplete M (AdicCompletion M R)

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

The adic completion of a Noetherian local ring is M-adically precomplete.

Part 4: Main theorem — IsNoetherianRing R̂

noncomputable def buildAdicSeq {α : Type u_3} {P : ℕ → α → Prop} (base : { a : α // P 0 a }) (step : (K : ℕ) → { a : α // P K a } → { a : α // P (K + 1) a }) (K : ℕ) : { a : α // P K a }

Generic helper: build a recursive sequence with proof-carrying data. This is a standalone def so its elaboration budget is independent.

Equations

• buildAdicSeq base step K = Nat.rec base (fun (K : ℕ) (prev : { a : α // P K a }) => step K prev) K

theorem filtration_smul_le (R : Type u_2) [CommRing R] (Mi : Ideal R) (J : Ideal (AdicCompletion Mi R)) (FN : ℕ → Ideal R) (hFN_def : ∀ (n : ℕ), FN n = Mi ^ n ⊓ Ideal.comap (Ideal.Quotient.mk (Mi ^ (n + 1))) (Ideal.map (AdicCompletion.evalₐ Mi (n + 1)).toRingHom J)) (n : ℕ) : Mi * FN n ≤ FN (n + 1)

theorem evalₐ_mk_smul_eq (R : Type u_2) [CommRing R] (Mi : Ideal R) (n0 K : ℕ) (m s : R) (hm : m ∈ Mi ^ K) (δ_s : AdicCompletion Mi R) (hδ_s_eq : (AdicCompletion.evalₐ Mi (n0 + 1)) δ_s = (Ideal.Quotient.mk (Mi ^ (n0 + 1))) s) : (Ideal.Quotient.mk (Mi ^ (n0 + K + 1))) m * (AdicCompletion.evalₐ Mi (n0 + K + 1)) δ_s = (Ideal.Quotient.mk (Mi ^ (n0 + K + 1))) (m • s)

theorem smul_lift_of_filtration (R : Type u_2) [CommRing R] (Mi : Ideal R) (n0 K : ℕ) (FN_n0 : Ideal R) (S_F : Finset R) (hS_F : Ideal.span ↑S_F = FN_n0) (I₀ : Ideal (AdicCompletion Mi R)) (hlift_span : ∀ t ∈ Ideal.span ↑S_F, ∃ δ ∈ I₀, (AdicCompletion.evalₐ Mi (n0 + 1)) δ = (Ideal.Quotient.mk (Mi ^ (n0 + 1))) t) (r' : R) (hr' : r' ∈ Mi ^ K • FN_n0) : ∃ δ ∈ I₀, (AdicCompletion.evalₐ Mi (n0 + K + 1)) δ = (Ideal.Quotient.mk (Mi ^ (n0 + K + 1))) r'

theorem coeff_decomp_of_smul (R : Type u_2) [CommRing R] (Mi : Ideal R) (n0 K : ℕ) (FN_n0 : Ideal R) (S_F : Finset R) (hS_F : Ideal.span ↑S_F = FN_n0) (genS : Finset (AdicCompletion Mi R)) (I₀ : Ideal (AdicCompletion Mi R)) (hI₀_eq : I₀ = Ideal.span ↑genS) (hlift_span : ∀ t ∈ Ideal.span ↑S_F, ∃ δ ∈ I₀, (AdicCompletion.evalₐ Mi (n0 + 1)) δ = (Ideal.Quotient.mk (Mi ^ (n0 + 1))) t) (r' : R) (hr' : r' ∈ Mi ^ K • FN_n0) : ∃ (c : AdicCompletion Mi R → AdicCompletion Mi R), (∀ g ∈ genS, c g ∈ Ideal.map (algebraMap R (AdicCompletion Mi R)) Mi ^ K) ∧ (AdicCompletion.evalₐ Mi (n0 + K + 1)) (∑ g ∈ genS, c g * g) = (Ideal.Quotient.mk (Mi ^ (n0 + K + 1))) r'

theorem extract_filtration_rep (R : Type u_2) [CommRing R] (Mi : Ideal R) (J : Ideal (AdicCompletion Mi R)) (FN : ℕ → Ideal R) (n0 K : ℕ) (hFN_def : ∀ (n : ℕ), FN n = Mi ^ n ⊓ Ideal.comap (Ideal.Quotient.mk (Mi ^ (n + 1))) (Ideal.map (AdicCompletion.evalₐ Mi (n + 1)).toRingHom J)) (FN_n0_sub : Submodule R R) (hn0_pow : ∀ (K : ℕ), Mi ^ K • FN_n0_sub = (fun (n : ℕ) => FN n) (n0 + K)) (Mhat : Ideal (AdicCompletion Mi R)) (hker_eq : ∀ (N : ℕ), RingHom.ker (AdicCompletion.evalₐ Mi N).toRingHom = Mhat ^ N) (e : AdicCompletion Mi R) (he : e ∈ Mhat ^ (n0 + K)) (heJ : e ∈ J) : ∃ r ∈ Mi ^ K • FN_n0_sub, (AdicCompletion.evalₐ Mi (n0 + K + 1)) e = (Ideal.Quotient.mk (Mi ^ (n0 + K + 1))) r

instance adicCompletion_isNoetherianRing (R : Type u_2) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] : IsNoetherianRing (AdicCompletion (IsLocalRing.maximalIdeal R) R)

The adic completion of a Noetherian local ring is Noetherian.