Commit 2024-07-01 12:34 60c9d3db

View on Github →

feat(RingTheory/AdicCompletion): exactness properties of adic completions (#12650) Shows:

adic completion preserves surjectivity
adic completion is exact if the base ring is Noetherian and the modules are finitely generated.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Exact.lean

added theorem Function.Exact.of_comp_eq_zero_of_ker_in_range

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

added theorem AdicCompletion.mk_zero_of

Created Mathlib/RingTheory/AdicCompletion/Exactness.lean

added theorem AdicCompletion.map_exact

added theorem AdicCompletion.map_injective

added theorem AdicCompletion.map_surjective

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

added theorem AdicCompletion.AdicCauchySequence.map_zero

added theorem AdicCompletion.map_zero