Zulip Chat Archive

Stream: new members

Topic: Flat modules


view this post on Zulip 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?

view this post on Zulip Heather Macbeth (Nov 01 2020 at 22:07):

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?

view this post on Zulip Heather Macbeth (Nov 01 2020 at 22:11):

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.

view this post on Zulip 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.

view this post on Zulip 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:
https://github.com/leanprover-community/mathlib/compare/flat-module

view this post on Zulip Heather Macbeth (Nov 01 2020 at 22:29):

(click on "files changed")

view this post on Zulip Roman Fedorov (Nov 01 2020 at 22:49):

Thanks!

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 02 2020 at 05:47):

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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Roman Fedorov (Nov 03 2020 at 16:10):

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

view this post on Zulip Johan Commelin (Nov 03 2020 at 16:13):

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

view this post on Zulip Roman Fedorov (Nov 03 2020 at 16:31):

https://pastebin.com/e9j44FLQ

view this post on Zulip Kenny Lau (Nov 03 2020 at 16:32):

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

view this post on Zulip Roman Fedorov (Nov 03 2020 at 16:58):

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

view this post on Zulip Johan Commelin (Nov 03 2020 at 17:00):

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

view this post on Zulip Johan Commelin (Nov 03 2020 at 17:00):

Are they the same file?

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (Nov 03 2020 at 17:06):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 03 2020 at 17:22):

The problem with my code is that it still contains gaps

view this post on Zulip Johan Commelin (Nov 03 2020 at 17:22):

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

view this post on Zulip Johan Commelin (Nov 03 2020 at 17:23):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 03 2020 at 17:40):

yup, fine with me

view this post on Zulip Johan Commelin (Nov 03 2020 at 17:41):

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

view this post on Zulip 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
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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 06 2020 at 09:35):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Roman Fedorov (Nov 13 2020 at 18:20):

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

view this post on Zulip 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: May 08 2021 at 04:14 UTC