## 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):

https://leanprover-community.github.io/contribute/index.html

#### 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.

#### 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:
https://github.com/leanprover-community/mathlib/compare/flat-module

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

(click on "files changed")

Thanks!

#### 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 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):

https://pastebin.com/e9j44FLQ

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

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

#### 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
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 (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: May 08 2021 at 04:14 UTC