Exactness of adic completion

In this file we establish exactness properties of adic completions. In particular we show:

Main results

• AdicCompletion.map_surjective: Adic completion preserves surjectivity.
• AdicCompletion.map_injective: Adic completion preserves injectivity of maps between finite modules over a Noetherian ring.
• AdicCompletion.map_exact: Over a Noetherian ring adic completion is exact on finite modules.

Implementation details

All results are proven directly without using Mittag-Leffler systems.

theorem AdicCompletion.map_surjective {R : Type u} [CommRing R] (I : Ideal R) {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑((map I) f)

Adic completion preserves surjectivity

theorem AdicCompletion.map_injective {R : Type u} [CommRing R] (I : Ideal R) {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] [IsNoetherianRing R] [Module.Finite R N] {f : M →ₗ[R] N} (hf : Function.Injective ⇑f) : Function.Injective ⇑((map I) f)

Adic completion preserves injectivity of finite modules over a Noetherian ring.

theorem AdicCompletion.map_exact {R : Type u} [CommRing R] {I : Ideal R} {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {P : Type u} [AddCommGroup P] [Module R P] [IsNoetherianRing R] [Module.Finite R N] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) : Function.Exact ⇑((map I) f) ⇑((map I) g)

AdicCompletion over a Noetherian ring is exact on finitely generated modules.