Completeness of the Adic Completion for Finitely Generated Ideals

This file establishes that AdicCompletion I M is itself I-adically complete when the ideal I is finitely generated.

Main definitions

• AdicCompletion.ofPowSMul: The canonical inclusion between adic completions induced by the inclusion from I ^ n • M to M.

• AdicCompletion.ofValEqZero: Given x in AdicCompletion I M projecting to zero in M / I ^ n • M, ofValEqZero constructs the corresponding element in the adic completion of I ^ n • M.

Main results

• AdicCompletion.pow_smul_top_eq_ker_eval: I ^ n • AdicCompletion I M is exactly the kernel of the evaluation map eval I M n when I is finitely generated.

• AdicCompletion.isAdicComplete: AdicCompletion I M is I-adically complete if I is finitely generated.

@[reducible, inline]

noncomputable abbrev AdicCompletion.ofPowSMul {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] (n : ℕ) : AdicCompletion I ↥(I ^ n • ⊤) →ₗ[AdicCompletion I R] AdicCompletion I M

The canonical inclusion from the adic completion of I ^ n • M to the adic completion of M.

theorem AdicCompletion.ofPowSMul_val_apply {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {a b c : ℕ} (h : c = b + a) {x : AdicCompletion I ↥(I ^ a • ⊤)} : ↑((ofPowSMul I M a) x) c = (Submodule.powSMulQuotInclusion I M h ⊤) (↑x b)

theorem AdicCompletion.ofPowSMul_val_apply_eq_zero {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {a b : ℕ} (h : a ≤ b) {x : AdicCompletion I ↥(I ^ b • ⊤)} : ↑((ofPowSMul I M b) x) a = 0

theorem AdicCompletion.ofPowSMul_injective {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] (n : ℕ) : Function.Injective ⇑(ofPowSMul I M n)

noncomputable def AdicCompletion.ofValEqZeroAux {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {a b c : ℕ} {x : AdicCompletion I M} (h : c = b + a) (ha : ↑x a = 0) : ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤

An auxillary lift function used in the definition of ofValEqZero. Use ofValEqZero instead.

noncomputable def AdicCompletion.ofValEqZero {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {n : ℕ} {x : AdicCompletion I M} (hxn : ↑x n = 0) : AdicCompletion I ↥(I ^ n • ⊤)

Given an element x in the adic completion of M whose projection to M / I ^ n • M is zero, ofValEqZero constructs the corresponding element in the adic completion of I ^ n • M.

@[simp]

theorem AdicCompletion.ofPowSMul_ofValEqZero {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {n : ℕ} {x : AdicCompletion I M} (hxn : ↑x n = 0) : (ofPowSMul I M n) (ofValEqZero I hxn) = x

theorem AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {n : ℕ} : Submodule.restrictScalars R (ofPowSMul I M n).range = (eval I M n).ker

theorem AdicCompletion.pow_smul_top_eq_ker_eval {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {n : ℕ} (h : I.FG) : I ^ n • ⊤ = (eval I M n).ker

Stacks Tag 05GG ((2))

theorem AdicCompletion.isAdicComplete {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] (h : I.FG) : IsAdicComplete I (AdicCompletion I M)

AdicCompletion I M is adic complete when I is finitely generated.