Flat modules

Stream: new members

[Roman Fedorov]

Hi, I wrote some code for flat modules over commutative rings (definition and a couple of basic theorems). I wonder if the community is OK with me adding that to mathlib?

[Heather Macbeth]

I am sure the answer will be yes. Have you seen this page
https://leanprover-community.github.io/contribute/index.html
outlining the process? Do you need write access to mathlib branches, if so what is your Github username?

[Heather Macbeth]

I believe @Johan Commelin has some work in progress on flat modules,
https://github.com/leanprover-community/mathlib/tree/flat-module
so some co-ordination might be required.

[Roman Fedorov]

@Johan Commelin , I went to this branch but could not find where flat modules are defined. Probably my lack of experience with github.

[Heather Macbeth]

Ah, sorry, here's the trick: find the "compare" button. This takes you to a page with Johan's additions clearly marked:
https://github.com/leanprover-community/mathlib/compare/flat-module

[Heather Macbeth]

(click on "files changed")

[Roman Fedorov]

Thanks!

[Kevin Buzzard]

One issue will be that there are several mathematically equivalent definitions of a flat module and someone who knows about the subtleties of these things will have to make a decision about what the best definition is from a formalisation point of view

[Johan Commelin]

@Roman Fedorov Cool! Do you have a link to your code somewhere?

[Roman Fedorov]

@Johan Commelin Here is the link: https://drive.google.com/file/d/1y0l7l9WgK05wJRoy1kpY21t6kzBvDuFD/view?usp=sharing. I have done much less than you (and I am using a different definition of flat module, though I guess you prove it is equivalent). I have proved that tensor product of flat modules is flat and that a non-zero divisor remains a non-zero divisor in a flat module (basically, I just wanted to play a bit with the definition to see that nothing breaks). But I guess my proofs are too long as I don't know how to use all that automation.

[Johan Commelin]

@Roman Fedorov When I go to that link google asks me to login, but I don't have a google login. Any chance you could upload it somewhere else? (For example pastebin.com or a github gist.)

[Roman Fedorov]

Is it better? https://drive.google.com/file/d/1y0l7l9WgK05wJRoy1kpY21t6kzBvDuFD/view?usp=sharing

[Johan Commelin]

It seems to be loading forever... can't you just paste the file in pastebin.com?

[Roman Fedorov]

https://pastebin.com/e9j44FLQ

[Kenny Lau]

if you upload it in gist you can enable Lean syntax highlighting

[Roman Fedorov]

@Johan Commelin @Kenny Lau https://gist.github.com/rmfedorov/6dae5d559bd0dafd9f87300bf1e537ad@

[Johan Commelin]

@Roman Fedorov thanks... I'm looking at the pastebin. The gist gives me a 404.

[Johan Commelin]

Are they the same file?

[Johan Commelin]

@Roman Fedorov Seems like you've written quite a lot of code already! It would be good to try to merge our efforts. (But I have almost no time for this atm.)

[Johan Commelin]

There is some overlap, but both approaches also do stuff that the other doesn't

[Roman Fedorov]

@Johan Commelin I figured out the issue with gist. I would be glad to put my code into your file (after re-working my code obviously). Should I just do it and put the result on gist?

[Bryan Gin-ge Chen]

The gist link works if you remove the @ at the end of the URL: https://gist.github.com/rmfedorov/6dae5d559bd0dafd9f87300bf1e537ad

[Johan Commelin]

The problem with my code is that it still contains gaps

[Johan Commelin]

I was trying to prove https://stacks.math.columbia.edu/tag/00HD

[Johan Commelin]

And then I got sidetracked into #4771 and #4773 about tensoring linear maps

[Bryan Gin-ge Chen]

Maybe @Roman Fedorov could work directly on @Johan Commelin 's branch (or a new branch derived from it)? The advantage of working on a branch of mathlib is that our automation will run on each commit to see if it builds, and it will also make future collaboration easier.

[Johan Commelin]

yup, fine with me

[Johan Commelin]

But like I said, my branch is a bit of a mess.

[Heather Macbeth]

@Roman Fedorov, here is a little more detail on how to edit Johan's branch (as Bryan suggests). Basically you follow the instructions in Step 6 at
https://leanprover-community.github.io/contribute/index.html
but with one difference: at the first step, instead of typing leanproject get -b mathlib:shiny_lemma, you type leanproject get mathlib:flat-module (i.e., leave out the -b), because instead of starting a fresh branch for your changes, you are going to be making changes on an existing branch.

You'll need write access to non-master branches (Step 3), so let us know if you're planning to do this, and someone will set it up for you.

[Eric Wieser]

It might be nice to PR injective_of_comp_bijective from that gist (or Johan's branch which has something very similar) independently, since that might be generally useful to people working on other things

[Johan Commelin]

Feel free to PR whatever you find useful from my branch!

[Roman Fedorov]

@Johan Commelin @Heather Macbeth Thanks! I am now trying to understand the details of the code; it will take me a few days.

[Roman Fedorov]

@Heather Macbeth , the "leanproject get..." command gives me "invalid git branch" after a while. Will write access help?

[Bryan Gin-ge Chen]

@Roman Fedorov I've just sent you an invite for mathlib: https://github.com/leanprover-community/mathlib/invitations

I'm not sure what could be causing "invalid git branch" though. Could you describe the steps you took in more detail?

[Roman Fedorov]

@Bryan Gin-ge Chen , thanks, it helped!

[Roman Fedorov]

@Johan Commelin So I committed two theorems :-) My code is probably very suboptimal as I am not good at using tactics