Tensor Products of modules and rings

Stream: mathlib4

[Antoine Chambert-Loir]

A few suggestions regarding the organization of tensor products in mathlib.

1. I just reproved (a particular case) of docs#TensorProduct.directLimitLeft (proved by @Jujian Zhang ) which belongs to a file in the file#Mathlib/Algebra/Module folder. I suggest that this file, file#Mathlib/Algebra/Module/DirectLimitAndTensorProduct be moved to LinearAlgebra.TensorProduct.DirectLimit

2. The file file#Mathlib/LinearAlgebra/TensorProduct exists, but also the folder. Would it be reasonable to move that file to Mathlib.LinearAlgebra.TensorProduct.Basic.lean?
   Or — in the opposite, each Basic file of a folder could be accessed by just typing the folder name?

3. If the preceding suggestion is accepted, move file#Mathlib/RingTheory/TensorProduct to Mathlib.RingTheory.TensorProduct.Basic.lean.
   In any case, there will be results about tensor products of rings sooner or later.

4. The file file#Mathlib/RingTheory/IsTensorProduct is essentially about base change of modules and rings, and I guess two foldersMathlib.LinearAlgebra.BaseChange and Mathlib.RingTheory.BaseChange would be appropriate, or maybe just Mathlib.Algebra.BaseChange and base change results for properties (flatness, etc.) would be in their respective folders.

[Antoine Chambert-Loir]

(If you tell me how to link to a file, I'll make the links and delete this comment , file#Mathlib/Algebra/Module/DirectLimitAndTensorProduct doesn't link to https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/DirectLimitAndTensorProduct.html but to something in tqft.net — https://tqft.net/mathlib4files/Mathlib/Algebra/Module.)

[Riccardo Brasca]

You can write something like file#Mathlib/Algebra/Module/DirectLimitAndTensorProduct, but it links to the source code.

[Riccardo Brasca]

https://tqft.net/ is Scott's website, I think there is a script or something that gives the link we want.

[Eric Wieser]

For 2., by "section" I assume you mean "folder" not "section"?

[Antoine Chambert-Loir]

yes, edited.

[Johan Commelin]

Ad 1: sounds good to me
Ad 2+3: yes, moving to Basic.lean fits the model we use elsewhere in mathlib
Ad 4: such a split makes sense to me

[Eric Wieser]

My opinion is that creating these Basic files is just import churn, and breaks downstream users (and creates minor merge conflicts) just to introduce a meaningless name

[Johan Commelin]

In general I have a slight uncomfy feeling about having a folder quux/foo/ and a file quux/foo.xyz in my filesystem. Probably just nonsense, but and I find it hard to specify the feeling further...

[Johan Commelin]

We already have Mathlib.lean and Mathlib/, so I should probably just get over this.

[Eric Wieser]

Johan Commelin said:

In general I have a slight uncomfy feeling about having a folder quux/foo/ and a file quux/foo.xyz in my filesystem. Probably just nonsense, but and I find it hard to specify the feeling further...

I guess this is an argument in favor of default.lean, which was removed in Lean 4

[Antoine Chambert-Loir]

I put points 1, 2 and 3 in #11282