[Merged by Bors] - refactor(*): rename `semimodule` to `module`, delete typeclasses `module` and `vector_space` #7322

Vierkantor · 2021-04-22T10:12:46Z

Splitting typeclasses between semimodule, module and vector_space was causing many (small) issues, so why don't we just get rid of this duplication?

This PR contains the following changes:

delete the old module and vector_space synonyms for semimodule
find and replace all instances of semimodule and vector_space to module
(thereby renaming the previous semimodule typeclass to module)
rename vector_space.dim to module.rank (in preparation for generalizing this definition to all modules)
delete a couple module instances that have now become redundant

This find-and-replace has been done extremely naïvely, but it seems there were almost no name clashes and no "clbuttic mistakes". I have gone through the full set of changes, finding nothing weird, and I'm fixing any build issues as they come up (I expect less than 10 declarations will cause conflicts).

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20from.20semimodule.20over.20a.20ring

A good example of a workaround required by the module abbreviation is the triv_sq_zero_ext.module instance.

…tor_space` Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20from.20semimodule.20over.20a.20ring

src/algebra/free_algebra.lean

test/free_algebra.lean

src/linear_algebra/dimension.lean

src/algebra/module/basic.lean

src/linear_algebra/dual.lean

src/linear_algebra/exterior_algebra.lean

src/linear_algebra/linear_independent.lean

src/linear_algebra/tensor_algebra.lean

sgouezel · 2021-04-23T10:31:04Z

docs/undergrad.yaml

-    vector space: 'vector_space'
-    product of vector spaces: 'prod.semimodule'
+    vector space: 'module'
+    product of vector spaces: 'prod.module'


Isn't that an unusual name? module.prod would be more standard.

It is the module instance on the prod type, therefore prod.module.

Vierkantor · 2021-04-23T12:40:06Z

Marking this as ready to review since it builds and the reaction on Zulip was positive.

sgouezel

This looks good to me, thanks a lot!
There is only one point about which I am unsure. After your refactor, we have both module.rank and findim, which don't go well together. Would finrank make sense? (And also adding somewhere a docstring saying that dimension is called rank, that would have enough keywords in it to be easy to find by grepping?)

src/algebra/module/ordered.lean

src/algebra/module/projective.lean

src/analysis/normed_space/basic.lean

src/linear_algebra/dimension.lean

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Vierkantor · 2021-04-23T15:09:32Z

After your refactor, we have both module.rank and findim, which don't go well together. Would finrank make sense?

I guess I might as well go ahead and change that. Can the finite_dimensional typeclass stay as it is, or also become finite_rank? (Does it hold for all modules that they have finite rank iff they are Noetherian?)

(And also adding somewhere a docstring saying that dimension is called rank, that would have enough keywords in it to be easy to find by grepping?)

In the docstring for module.rank I wrote: "In a vector space, this is the same as the dimension of the space." Do you have suggestions for something to add?

We still call keep calling `finite_dimensional` the same thing, but we might decide to change that later.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

sgouezel · 2021-04-23T18:53:49Z

Looks like the linter is not happy. Otherwise, let's get this merged quickly to avoid incoming conflicts.
bors d+

bors · 2021-04-23T18:53:50Z

✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

sgouezel · 2021-04-24T07:48:10Z

bors r+

…ule` and `vector_space` (#7322) Splitting typeclasses between `semimodule`, `module` and `vector_space` was causing many (small) issues, so why don't we just get rid of this duplication? This PR contains the following changes: * delete the old `module` and `vector_space` synonyms for `semimodule` * find and replace all instances of `semimodule` and `vector_space` to `module` * (thereby renaming the previous `semimodule` typeclass to `module`) * rename `vector_space.dim` to `module.rank` (in preparation for generalizing this definition to all modules) * delete a couple `module` instances that have now become redundant This find-and-replace has been done extremely naïvely, but it seems there were almost no name clashes and no "clbuttic mistakes". I have gone through the full set of changes, finding nothing weird, and I'm fixing any build issues as they come up (I expect less than 10 declarations will cause conflicts). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20from.20semimodule.20over.20a.20ring A good example of a workaround required by the `module` abbreviation is the [`triv_sq_zero_ext.module` instance](https://github.com/leanprover-community/mathlib/blob/3b8cfdc905c663f3d99acac325c7dff1a0ce744c/src/algebra/triv_sq_zero_ext.lean#L164). Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

bors · 2021-04-24T10:15:57Z

Build failed:

Build mathlib

sgouezel · 2021-04-24T15:20:18Z

bors r+ p=37

…ule` and `vector_space` (#7322) Splitting typeclasses between `semimodule`, `module` and `vector_space` was causing many (small) issues, so why don't we just get rid of this duplication? This PR contains the following changes: * delete the old `module` and `vector_space` synonyms for `semimodule` * find and replace all instances of `semimodule` and `vector_space` to `module` * (thereby renaming the previous `semimodule` typeclass to `module`) * rename `vector_space.dim` to `module.rank` (in preparation for generalizing this definition to all modules) * delete a couple `module` instances that have now become redundant This find-and-replace has been done extremely naïvely, but it seems there were almost no name clashes and no "clbuttic mistakes". I have gone through the full set of changes, finding nothing weird, and I'm fixing any build issues as they come up (I expect less than 10 declarations will cause conflicts). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20from.20semimodule.20over.20a.20ring A good example of a workaround required by the `module` abbreviation is the [`triv_sq_zero_ext.module` instance](https://github.com/leanprover-community/mathlib/blob/3b8cfdc905c663f3d99acac325c7dff1a0ce744c/src/algebra/triv_sq_zero_ext.lean#L164). Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

bors · 2021-04-24T19:36:48Z

Pull request successfully merged into master.

Build succeeded:

… of `dim` (#18735) The `dim` name is left from the previous name of the function, `vector_space.dim`. When that was merged with `module.rank` in #7322, we left renaming the existing lemmas as future work. This commit was made by replacing `(\b|(?<=_))dim(\b|(?=_))` with `rank` in the `dimension` and `finite_dimensional` files, and then manually fixing downstream breakages; it's important not to rename `power_basis.dim` at the same time! Deciding whether to move some of these to the `module` namespace is left as future work, the diff is already big enough.

… of `dim` (#18741) The `dim` name is left from the previous name of the function, `vector_space.dim`. When that was merged with `module.rank` in #7322, we left renaming the existing lemmas as future work. This commit was made by replacing `(\b|(?<=_))dim(\b|(?=_))` with `rank` in the `dimension` and `finite_dimensional` files, and then manually fixing downstream breakages; it's important not to rename `power_basis.dim` at the same time! Deciding whether to move some of these to the `module` namespace is left as future work, the diff is already big enough.

Rename semimodule to module, delete typeclasses module and `vec…

e1f0dff

…tor_space` Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20from.20semimodule.20over.20a.20ring

Vierkantor added WIP Work in progress RFC Request for comment labels Apr 22, 2021