PolynomialModule equiv TensorProduct

Stream: mathlib4

[George McNinch]

Hi,
So, I have a proof of the following that I'd like to submit as a PR to Mathlib:

variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]

def TensorProductEquivPolynomialModule : (R[X] ⊗[R] M) ≃ₗ[R[X]] (PolynomialModule R M)

(Well, that it is not only that def that I want to submit, but that is the main result).

This will be my first Mathlib PR and I guess I'm asking for tips on "how to proceed"...! (Hope I've posted this in at least a somewhat reasonable place...)

• Maybe a first comment to make is this: I never got the notation M[X] to work ... so I just wrote PolynomialModule R M everywhere. That seems consistent with the code that I see here, though not with all of the prose.
• I expect that I could use some guidance I'm aware of the contribution guidlines and I know there are still things that need to be done before I actually make the pull-request (at least: name-changes and inclusion of module-level docstring...) But I'm a bit vague on a few things:
  • sections and namespaces. (I mean, I believe I understand what they do. But it is not completely clear e.g. in my case whether to put everything in the PolynomialModule name space, or what...)
  • imports: if e.g. in the PR I added a new file to Mathlib/Algebra/Polynomial/Module do I need to add an import line for that file to Mathlib.lean? (Seems a bit unlikely, but I'm not sure how the relevant import statement would get there...)
• you can see my code here

[Kenny Lau]

I'm always in favour of more notation: I suppose M[X] wouldn't work because of conflict with R[X], but what about M[X]_R?

[Kenny Lau]

George McNinch said:

• do I need to add an import line for that file to Mathlib.lean

yes, but it's supposed to be automatic once you run the command lake exe mk_all

[Kenny Lau]

George McNinch said:

• sections and namespaces.

it will be more clear in the context of a PR

[Kim Morrison]

Contrary to what Kenny says (I am always against more notation :-), don't worry about improving the notational situation if you are fighting against it. PolynomialModule is fine for your PR.

[George McNinch]

Kim Morrison said:

Contrary to what Kenny says (I am always against more notation :-), don't worry about improving the notational situation if you are fighting against it. PolynomialModule is fine for your PR.

Right; thanks. My PR isn't going to propose any notation!

[Kenny Lau]

a middle path could be local notation :melt:

[Eric Wieser]

It's still usually best to develop the mathematics in separate PRs from the notation

[George McNinch]

Kenny Lau said:

George McNinch said:

• do I need to add an import line for that file to Mathlib.lean

yes, but it's supposed to be automatic once you run the command lake exe mk_all

Aha that makes sense.

[George McNinch]

So I've made the PR. First round, I had some whitespace at the end of lines, which I fixed and updated the commite. The lint-check now passes.

But now there is an error in the build, as follows:

Run if [[ "skipped" != "success" ]]; then
+ [[ skipped != \s\u\c\c\e\s\s ]]
+ echo 'Please run '\''lake exe mk_all'\'' to regenerate the import all files'
+ exit 1
Please run 'lake exe mk_all' to regenerate the import all files

Error: Process completed with exit code 1.

I did run lake exe mk_all before the commit. I didn't re-run it after fixing the whitespace issues though.

But the error message seems to tell me to rerun it, but when I do so I get:

george@valhalla:~/Prof-VC/mathlib4$ lake exe mk_all
No update necessary

george@valhalla:~/Prof-VC/mathlib4$ git status
On branch PolyModuleTensor
Your branch is up to date with 'origin/PolyModuleTensor'.
nothing to commit, working tree clean

and there is a line import Mathlib.Algebra.Polynomial.Module.TensorProduct in Mathlib.lean.

Any suggestion as to how to proceed?

[Aaron Liu]

Try merging master?

[George McNinch]

Aaron Liu said:

Try merging master?

Good idea, but unfortunately didn't work. (pulling on the master branch didn't produce any changes)

[George McNinch]

Nevermind for now -- I see the problem. I had import Mathlib at the top of the file.

Just before making the PR, I ran lake build which worked, and then ran lake exe mk_all.
I didn't try lake build again, but a subsequent lake build fails because of bad import.

So I just need to work out required imports.

Sorry for the noise!

[George McNinch]

OK --my PR is all set. Thanks all around for the help/advice etc.