[Merged by Bors] - feat(RingTheory/AdicCompletion): adic completion of Noetherian ring is flat

[chrisflav]

We show that the adic completion of a Noetherian ring R is flat.

More precisely, we show that on finite modules over a Noetherian ring, tensoring a module M with the adic completion of R is the same as adically completing M. From this we conclude since adic completion on such modules is exact.

Co-authored-by: Judith Ludwig [email protected]

---

• depends on: [Merged by Bors] - feat(RingTheory/AdicCompletion): comparison with tensor product #14358

[github-actions]

PR summary dd8f45e97e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.AdicCompletion.AsTensorProduct	1172	1557	+385 (+32.85%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.AdicCompletion.AsTensorProduct	385

---

Declarations diff

+ flat_of_isNoetherian
+ isIso_of_isInitial
+ isIso_of_isTerminal
+ lTensorKerIncl
+ ofTensorProductEquivOfFiniteNoetherian
+ ofTensorProductEquivOfFiniteNoetherian_apply
+ ofTensorProductEquivOfFiniteNoetherian_symm_of
+ ofTensorProduct_bijective_of_finite_of_isNoetherian
+ ofTensorProduct_bijective_of_map_from_fin
+ ofTensorProduct_surjective_of_finite
+ tensor_map_id_left_eq_map
+ tensor_map_id_left_injective_of_injective
- ofTensorProduct_surjective_of_fg

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(RingTheory/AdicCompletion): comparison with tensor product #14358
  By Dependent Issues (🤖). Happy coding!

[riccardobrasca]

LGTM. My only question is whether it makes sense to keep on proving stuff about the completion rather than introducing a predicate IsAdicCompletion: we will surely want it, and you are just adding more work to adapt everything.

[chrisflav]

LGTM. My only question is whether it makes sense to keep on proving stuff about the completion rather than introducing a predicate IsAdicCompletion: we will surely want it, and you are just adding more work to adapt everything.

I agree, this is the last PR in this series though. Also I think that the flatness can be rather easily obtained for IsAdicCompletion by just transferring via the isomorphism.

[riccardobrasca]

bors d+

[mathlib-bors]

✌️ chrisflav can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[chrisflav]

Thanks for the review!

bors r+

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style