Zulip Chat Archive

Stream: new members

Topic: Flat modules

Roman Fedorov (Nov 01 2020 at 21:57):

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 (Nov 01 2020 at 22:07):

I am sure the answer will be yes. Have you seen this page
outlining the process? Do you need write access to mathlib branches, if so what is your Github username?

Heather Macbeth (Nov 01 2020 at 22:11):

I believe @Johan Commelin has some work in progress on flat modules,
so some co-ordination might be required.

Roman Fedorov (Nov 01 2020 at 22:27):

@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 (Nov 01 2020 at 22:28):

Ah, sorry, here's the trick: find the "compare" button. This takes you to a page with Johan's additions clearly marked:

Heather Macbeth (Nov 01 2020 at 22:29):

(click on "files changed")

Roman Fedorov (Nov 01 2020 at 22:49):


Kevin Buzzard (Nov 01 2020 at 23:07):

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 (Nov 02 2020 at 05:47):

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

Roman Fedorov (Nov 03 2020 at 01:32):

@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 (Nov 03 2020 at 05:55):

@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 (Nov 03 2020 at 16:10):

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

Johan Commelin (Nov 03 2020 at 16:13):

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

Roman Fedorov (Nov 03 2020 at 16:31):


Kenny Lau (Nov 03 2020 at 16:32):

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

Roman Fedorov (Nov 03 2020 at 16:58):

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

Johan Commelin (Nov 03 2020 at 17:00):

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

Johan Commelin (Nov 03 2020 at 17:00):

Are they the same file?

Johan Commelin (Nov 03 2020 at 17:06):

@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 (Nov 03 2020 at 17:06):

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

Roman Fedorov (Nov 03 2020 at 17:18):

@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 (Nov 03 2020 at 17:20):

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

Johan Commelin (Nov 03 2020 at 17:22):

The problem with my code is that it still contains gaps

Johan Commelin (Nov 03 2020 at 17:22):

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

Johan Commelin (Nov 03 2020 at 17:23):

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

Bryan Gin-ge Chen (Nov 03 2020 at 17:40):

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 (Nov 03 2020 at 17:40):

yup, fine with me

Johan Commelin (Nov 03 2020 at 17:41):

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

Heather Macbeth (Nov 03 2020 at 18:17):

@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
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 (Nov 06 2020 at 09:24):

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 (Nov 06 2020 at 09:35):

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

Roman Fedorov (Nov 07 2020 at 00:18):

@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 (Nov 13 2020 at 17:20):

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

Bryan Gin-ge Chen (Nov 13 2020 at 17:27):

@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 (Nov 13 2020 at 18:20):

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

Roman Fedorov (Nov 13 2020 at 20:44):

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

Last updated: Dec 20 2023 at 11:08 UTC