feat(Topology/Algebra/Module/ClosedSubmodule): add mapEquiv, a variation of ClosedSubmodule.map for CLE

[yoh-tanimoto]

add ClosedSubmodule.mapEquiv for continuous linear equivalence. In this case, a closed submodule is mapped to a closed submodule, so the definitions are easier and behave nicely with closure and ⊔.

motivation: needed to define standard subspaces in a Hilbert space (scalar multiplication by Complex.I) #29251
https://ems.press/content/serial-article-files/48171

• depends on: [Merged by Bors] - feat(Topology/Algebra/Module/ClosedSubmodule): add instances Lattice CompleteLattice #29230 for Lattice CompleteLattice

[github-actions]

PR summary 976d30f376

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Algebra.Module.ClosedSubmodule	1185	1187	+2 (+0.17%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.Convex.Cone.Basic Mathlib.Topology.Algebra.Module.ClosedSubmodule	2

---

Declarations diff

+ closure_map_eq_mapEquiv_closure
+ mapEquiv
+ mapEquiv_apply
+ mapEquiv_bot_eq_bot
+ mapEquiv_inf_eq_inf_mapEquiv
+ mapEquiv_sup_eq_sup_mapEquiv
+ mapEquiv_symm
+ mapEquiv_top_eq_top
+ mem_mapEquiv_iff
+ mem_mapEquiv_iff'

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Topology/Algebra/Module/ClosedSubmodule): add instances Lattice CompleteLattice #29230
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[j-loreaux]

I'm out of time for today. Sorry, I will try to come back to it soon.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[yoh-tanimoto]

Should I define mapEquiv as mapEquiv (f : M ≃L[R] N) : Equiv (Submodule R M) (Submodule R N)?

I also noticed that there are map for AddMonoid and AddCommGroup. Should I define mapEquiv for them as well?

[j-loreaux]

Should I define mapEquiv as mapEquiv (f : M ≃L[R] N) : Equiv (Submodule M) (Submodule N)?

I also noticed that there are map for AddMonoid and AddCommGroup. Should I define mapEquiv for them as well?

That sounds like a pretty good idea. Of course, the others should happen in a separate PR.

[yoh-tanimoto]

Ok I changed it to Equiv. I will do the other stuff in another PR hopefully soon.