[Merged by Bors] - feat(RingTheory/LocalRing/Module): Finitely presented flat modules over local rings are free. #14375

erdOne · 2024-07-03T01:53:13Z

…er local rings are free.

github-actions · 2024-07-03T01:53:49Z

PR summary 812755553c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.LocalRing.Module`	1467

Declarations diff

+ LocalRing.split_injective_iff_lTensor_residueField_injective
+ TensorProduct.mk_surjective
+ free_of_flat_of_localRing
+ free_of_lTensor_residueField_injective
+ free_of_maximalIdeal_rTensor_injective
+ lTensor_injective_of_exact_of_exact_of_rTensor_injective
+ map_mkQ_eq
+ map_mkQ_eq_top
+ map_tensorProduct_mk_eq_top
+ span_eq_top_of_tmul_eq_basis
+ subsingleton_tensorProduct

You can run this locally as follows

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

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

faenuccio

I have read the first 200 lines of Module.lean up to the declaration Module.free_of_lTensor_residueField_injective

faenuccio · 2024-07-03T19:44:33Z

Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

@@ -419,6 +419,16 @@ theorem TensorProduct.map_ker :

 variable (M)

+variable (R) in


Any specific reason for putting R as a localized variable and leaving S inside the statement? What about having variable (R S) in before the theorem?

variable (R) in makes the variable explicit, but there is not a global variable {S} living around.

I agree, but variable (R S) has the same effect... Not very important, at any rate.

Mathlib/RingTheory/LocalRing/Module.lean

Co-authored-by: Filippo A. E. Nuccio <[email protected]>

Mathlib/RingTheory/LocalRing/Module.lean

faenuccio

Thanks so much for all the work!

Mathlib/RingTheory/LocalRing/Module.lean

faenuccio · 2024-07-04T06:45:40Z

Mathlib/RingTheory/LocalRing/Module.lean

+      rw [← LinearMap.lTensor_comp, hl, LinearMap.lTensor_id]
+    exact Function.HasLeftInverse.injective ⟨_, LinearMap.congr_fun this⟩
+  · intro h
+    -- By the lemma above, `k ⊗ l` injective => `N ⧸ l(M)` free.


Can you rather refer to the name of the declaration instead of "lemma above"?

It is directly on the next line though.
I've changed the wording a bit but I'll include the lemma name if you still think it's better to do so.

I think so, because in the future people might move things around and it won't be "above" anymore (and given the lack of attention that is normally taken at the doc, it is likely they would forget to update).

To clarify, the current wording is

-- By the a previously proved lemma, `k ⊗ l` injective => `N ⧸ l(M)` free. have := Module.free_of_lTensor_residueField_injective l (LinearMap.range l).mkQ

And you suggest

-- By `Module.free_of_lTensor_residueField_injective`, `k ⊗ l` injective => `N ⧸ l(M)` free. have := Module.free_of_lTensor_residueField_injective l (LinearMap.range l).mkQ

Yes, thanks!

Mathlib/RingTheory/LocalRing/Module.lean

faenuccio · 2024-07-05T07:59:21Z

maintainer merge

github-actions · 2024-07-05T07:59:33Z

🚀 Pull request has been placed on the maintainer queue by faenuccio.

erdOne · 2024-07-05T08:00:47Z

Thanks for the swift review!

jcommelin

Thanks 🎉

bors merge

riccardobrasca · 2024-07-05T08:53:28Z

Mathlib/RingTheory/LocalRing/Module.lean

+  rw [(LinearMap.exact_subtype_ker_map i).linearMap_comp_eq_zero]
+  simp only [LinearMap.lTensor_zero, LinearMap.zero_apply, map_zero]
+
+theorem free_of_flat_of_localRing [Module.FinitePresentation R P] [Module.Flat R P] :


I think this is true for any finite module, maybe we can add a TODO (the proof is much harder IIRC).

We're actually not that far away. We already have the equational criterion of flatness and finite flat = free is a (relatively) easy application of that. Anyways I added a TODO.

mathlib-bors · 2024-07-05T09:10:23Z

Canceled.

riccardobrasca · 2024-07-05T09:11:11Z

bors d+

mathlib-bors · 2024-07-05T09:11:13Z

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

erdOne · 2024-07-05T09:15:01Z

bors merge

…er local rings are free. (#14375) Co-authored-by: Andrew Yang <[email protected]>

mathlib-bors · 2024-07-05T09:32:03Z

Pull request successfully merged into master.

Build succeeded:

feat(RingTheory/LocalRing/Module): Finitely presented flat modules ov…

178507e

…er local rings are free.

erdOne added awaiting-review awaiting-CI t-algebra Algebra (groups, rings, fields, etc) labels Jul 3, 2024

line too long

8c134d9

github-actions bot removed the awaiting-CI label Jul 3, 2024

move lemma

b5cf0d3

faenuccio reviewed Jul 3, 2024

View reviewed changes

faenuccio self-assigned this Jul 3, 2024

Apply suggestions from code review

0df45c5

Co-authored-by: Filippo A. E. Nuccio <[email protected]>

erdOne added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jul 3, 2024

erdOne added 2 commits July 4, 2024 09:58

address comments

c2fad27

use namespace

5690074

erdOne added awaiting-review awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 4, 2024

github-actions bot removed the awaiting-CI label Jul 4, 2024

faenuccio reviewed Jul 4, 2024

View reviewed changes

Mathlib/RingTheory/LocalRing/Module.lean Outdated Show resolved Hide resolved

faenuccio reviewed Jul 4, 2024

View reviewed changes

Mathlib/RingTheory/LocalRing/Module.lean Outdated Show resolved Hide resolved

faenuccio reviewed Jul 4, 2024

View reviewed changes

Mathlib/RingTheory/LocalRing/Module.lean Outdated Show resolved Hide resolved

faenuccio reviewed Jul 4, 2024

View reviewed changes

Mathlib/RingTheory/LocalRing/Module.lean Outdated Show resolved Hide resolved

faenuccio reviewed Jul 4, 2024

View reviewed changes

faenuccio added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jul 4, 2024

address comments

8dc71aa

erdOne added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 4, 2024

Update comment

593e84d

github-actions bot added the maintainer-merge label Jul 5, 2024

faenuccio removed the awaiting-review label Jul 5, 2024

jcommelin reviewed Jul 5, 2024

View reviewed changes

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jul 5, 2024

riccardobrasca reviewed Jul 5, 2024

View reviewed changes

Update Module.lean

8127555

github-actions bot added the delegated label Jul 5, 2024

mathlib-bors bot pushed a commit that referenced this pull request Jul 5, 2024

feat(RingTheory/LocalRing/Module): Finitely presented flat modules ov…

46dd6da

…er local rings are free. (#14375) Co-authored-by: Andrew Yang <[email protected]>

mathlib-bors bot changed the title ~~feat(RingTheory/LocalRing/Module): Finitely presented flat modules over local rings are free.~~ [Merged by Bors] - feat(RingTheory/LocalRing/Module): Finitely presented flat modules over local rings are free. Jul 5, 2024

mathlib-bors bot closed this Jul 5, 2024

mathlib-bors bot deleted the erd1/localflat branch July 5, 2024 09:32

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

alreadydone mentioned this pull request Dec 20, 2024

[Merged by Bors] - chore(RingTheory/LocalRing): strengthen Module.free_of_flat_of_isLocalRing #19846

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(RingTheory/LocalRing/Module): Finitely presented flat modules over local rings are free. #14375

[Merged by Bors] - feat(RingTheory/LocalRing/Module): Finitely presented flat modules over local rings are free. #14375

erdOne commented Jul 3, 2024

github-actions bot commented Jul 3, 2024 •

edited

Loading

Declarations diff

faenuccio left a comment

faenuccio Jul 3, 2024

erdOne Jul 3, 2024

faenuccio Jul 4, 2024

faenuccio left a comment

faenuccio Jul 4, 2024

erdOne Jul 4, 2024

faenuccio Jul 5, 2024

erdOne Jul 5, 2024

faenuccio Jul 5, 2024 •

edited

Loading

faenuccio commented Jul 5, 2024

github-actions bot commented Jul 5, 2024

erdOne commented Jul 5, 2024

jcommelin left a comment

riccardobrasca Jul 5, 2024

erdOne Jul 5, 2024

mathlib-bors bot commented Jul 5, 2024

riccardobrasca commented Jul 5, 2024

mathlib-bors bot commented Jul 5, 2024

erdOne commented Jul 5, 2024

mathlib-bors bot commented Jul 5, 2024

		@@ -419,6 +419,16 @@ theorem TensorProduct.map_ker :

		variable (M)

		variable (R) in

[Merged by Bors] - feat(RingTheory/LocalRing/Module): Finitely presented flat modules over local rings are free. #14375

[Merged by Bors] - feat(RingTheory/LocalRing/Module): Finitely presented flat modules over local rings are free. #14375

Conversation

erdOne commented Jul 3, 2024

github-actions bot commented Jul 3, 2024 • edited Loading

PR summary 812755553c

Import changes for modified files

Declarations diff

faenuccio left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

faenuccio left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

faenuccio Jul 5, 2024 • edited Loading

Choose a reason for hiding this comment

faenuccio commented Jul 5, 2024

github-actions bot commented Jul 5, 2024

erdOne commented Jul 5, 2024

jcommelin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mathlib-bors bot commented Jul 5, 2024

riccardobrasca commented Jul 5, 2024

mathlib-bors bot commented Jul 5, 2024

erdOne commented Jul 5, 2024

mathlib-bors bot commented Jul 5, 2024

github-actions bot commented Jul 3, 2024 •

edited

Loading

faenuccio Jul 5, 2024 •

edited

Loading