mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: the equational criterion for flatness

Open trivial1711 opened this issue 1 year ago • 5 comments
trafficstars

We prove the equational criterion for flatness. As a consequence, every homomorphism from a finitely presented module to a flat module factors through a finite free module.

  • [x] depends on: #12647

Open in Gitpod

trivial1711 avatar May 05 '24 00:05 trivial1711

This PR/issue depends on:

  • ~~leanprover-community/mathlib4#12647~~ By Dependent Issues (🤖). Happy coding!

leanprover-community-mathlib4-bot avatar May 17 '24 06:05 leanprover-community-mathlib4-bot

Hello, I managed to make Algebra/Module/FinitePresentation.lean fully universe polymorphic. This had the side effect of somehow breaking RingTheory/Flat/EquationalCriterion.lean, even though I didn't even touch that file. I think this is almost certainly not worth it. #13149

trivial1711 avatar May 23 '24 19:05 trivial1711

Hello, I managed to make Algebra/Module/FinitePresentation.lean fully universe polymorphic. This had the side effect of somehow breaking RingTheory/Flat/EquationalCriterion.lean, even though I didn't even touch that file. I think this is almost certainly not worth it. #13149

Oh great, thanks! I think the extra leg-freedom in the universe level of the indexing type will pay off, but I think we can merge this PR and generalize in a second step with your follow-up PR.

chrisflav avatar May 23 '24 20:05 chrisflav

Hi, I'm sorry about the way I worded my comment earlier. I shouldn't be so dismissive about universe polymorphism; I now see it could very plausibly matter at some point. Do you have any suggestions for how to do #13149? You can make commits directly if you want.

trivial1711 avatar May 23 '24 23:05 trivial1711

Hi, I'm sorry about the way I worded my comment earlier. I shouldn't be so dismissive about universe polymorphism; I now see it could very plausibly matter at some point. Do you have any suggestions for how to do #13149? You can make commits directly if you want.

Currently I am busy, but I'll have a look in two days.

chrisflav avatar May 24 '24 07:05 chrisflav

Apart from one open question above, I think this is good to go. Since the universe generalizations depend on #13149, we can merge this one as is and generalize after #13149.

chrisflav avatar Jun 02 '24 17:06 chrisflav

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar Jun 04 '24 09:06 mathlib-bors[bot]