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)
:
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)
:
Function.Exact ⇑(AdicCompletion.map I f) ⇑(AdicCompletion.map I g)
AdicCompletion over a Noetherian ring is exact on finitely generated modules.