feat(RingTheory/Flat): faithfully flat ring maps

[judithludwig]

Add definition of faithfully flat ring maps and show basic properties. Co-authored-by: Florent Schaffhauser (github: matematiflo) Co-authored-by: Jujian Zhang (github:@jjaassoonn) Co-authored-by: Yunzhou Xie (github:@whysoserioushah)

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

---

• [x] depends on: #17803
• [x] depends on: #17805
• [x] depends on: #17484
• [x] depends on: #17869

[github-actions[bot]]

PR summary d2d43d9e9d

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Flat.FaithfullyFlat	1464	1477	+13 (+0.89%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.Flat.FaithfullyFlat	13

---

Declarations diff

+ comp + iff_zero_iff_lTensor_zero + iff_zero_iff_rTensor_zero + of_linearEquiv + zero_iff_lTensor_zero + zero_iff_rTensor_zero

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

[judithludwig]

There is the following alternative definition of faithfully flat ring map and there should probably be a discussion about which one should become the mathlib definition:

variable (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M]

@[mk_iff] class FaithfullyFlat' : Prop where
  flat : Module.Flat R M := by infer_instance
   submodule_ne_top :  ∀ ⦃m : Ideal R⦄ (_ : Ideal.IsMaximal m), m • (⊤ : Submodule R M) ≠ ⊤ 

This would avoid universe issues.

[riccardobrasca]

There is the following alternative definition of faithfully flat ring map and there should probably be a discussion about which one should become the mathlib definition:

variable (R : Type u) (M : Type v) [CommRing R] [AddCommGroup M] [Module R M]

@[mk_iff] class FaithfullyFlat' : Prop where
  flat : Module.Flat R M := by infer_instance
   submodule_ne_top :  ∀ ⦃m : Ideal R⦄ (_ : Ideal.IsMaximal m), m • (⊤ : Submodule R M) ≠ ⊤ 

This would avoid universe issues.

I think this second version is better. I understand that it is probably not easy to show the equivalence, but putting in mathlib a definition that we know we are going to change is a recipe to make people suffering (someone will start using your definition, and the refactor will be more and more painful).

Can you start adding the basic API to show equivalence? (Or anything else you need!). Thanks!

[judithludwig]

I think this second version is better. I understand that it is probably not easy to show the equivalence, but putting in mathlib a definition that we know we are going to change is a recipe to make people suffering (someone will start using your definition, and the refactor will be more and more painful).

Can you start adding the basic API to show equivalence? (Or anything else you need!). Thanks!

I'll label this PR as work in progress for now until we sort this out. Thanks for your input.

[jjaassoonn]

I just want some very quick and general comments about if these changes are in the right direction. If so, I will split this PR

[jcommelin]

I just want some very quick and general comments about if these changes are in the right direction. If so, I will split this PR

@jjaassoonn the general direction looks good to me.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#17803~~
• ~~leanprover-community/mathlib4#17805~~
• ~~leanprover-community/mathlib4#17484~~
• ~~leanprover-community/mathlib4#17869~~ By Dependent Issues (🤖). Happy coding!

[riccardobrasca]

Can you please fix the error?

[jjaassoonn]

Done, sorry was having late lunch

[mathlib-bors[bot]]

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

[jcommelin]

Thanks :tada:

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style