Adic completeness of finite modules

Over an I-adically complete Noetherian ring, every finitely generated module is I-adically complete. Precompleteness passes along surjective linear maps, because the adic completion functor preserves surjections; a finite module is a quotient of a finite free module, which is complete by IsAdicComplete.pi. Hausdorffness is the Krull intersection theorem (IsHausdorff.of_le_jacobson), available because I lies in the Jacobson radical of a complete ring.

This is what makes a finite algebra over a complete Noetherian ring Henselian along the extended ideal, the input for lifting idempotents in such an algebra.

Main results

• IsPrecomplete.of_surjective: adic precompleteness passes along a surjective linear map.
• IsPrecomplete.of_finite: a finite module over an adically precomplete ring is precomplete.
• IsAdicComplete.of_finite: a finite module over an adically complete Noetherian ring is complete.

References

• M. F. Atiyah, I. G. Macdonald, Introduction to Commutative Algebra, Chapter 10.

theorem IsPrecomplete.of_surjective {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsPrecomplete I M] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) : IsPrecomplete I N

Adic precompleteness passes along a surjective linear map: the adic completion functor preserves surjections.

theorem IsPrecomplete.of_finite {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [IsPrecomplete I R] [Module.Finite R M] : IsPrecomplete I M

A finite module over an I-adically precomplete ring is I-adically precomplete.

theorem IsAdicComplete.of_finite {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [IsAdicComplete I R] [Module.Finite R M] : IsAdicComplete I M

A finite module over an I-adically complete Noetherian ring is I-adically complete.