Documentation

Mathlib.RingTheory.AdicCompletion.Exactness

Exactness of adic completion #

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

Main results #

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) :

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) :

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) :

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