[Merged by Bors] - feat: topology on module over topological ring

[kbuzzard]

Given a module over a topological ring, we define the module topology on this module to be the finest module making it into a topological module (i.e. the finest topology making addition and scalar multiplication continuous).

NB this PR gave rise to a discussion about whether ⨆ a ∈ s, f a or sSup (f '' s) should be the simp normal form, which was discussed on Zulip without any clear conclusion.

---

I wanted this because for a finite free module it can be checked to be the product topology, and for an algebra over a commutative topological ring which is finite as a module, multiplication in the algebra is automatically continuous with this topology. I have all of these results in the FLT repo in this file. What inspired me to PR it to mathlib was Yael's question here -- this topology gives a very nice answer to that question.

[github-actions]

PR summary ef2b10cd79

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Algebra.Module.Basic	1030	1032	+2 (+0.19%)

Import changes for all files

Files	Import difference
15 files Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.Algebra.Module.Star Mathlib.Analysis.Convex.Exposed	2
Mathlib.Topology.Algebra.Module.ModuleTopology	1033

---

Declarations diff

+ IsModuleTopology
+ IsModuleTopology.toContinuousAdd
+ IsModuleTopology.toContinuousSMul
+ ModuleTopology.continuousAdd
+ ModuleTopology.continuousSMul
+ coinduced_sSup
+ eq_moduleTopology
+ induced_sInf
+ instSubsingleton
+ instance _root_.TopologicalSemiring.toIsModuleTopology : IsModuleTopology R R := by
+ instance _root_.TopologicalSemiring.toOppositeIsModuleTopology : IsModuleTopology Rᵐᵒᵖ R
+ iso
+ moduleTopology
+ moduleTopology_le
+ of_continuous_id
+ opContinuousLinearEquiv

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.

[eric-wieser]

bors d+

Thanks! I pushed two small golfs, feel free to merge before CI if they look fine to you. (I did test them)

[eric-wieser]

This is a long comment for a very small amount of proof!

[kbuzzard]

Yes, and in my opinion more of mathlib should look like this! The proof of continuousSMul_sInf is slightly subtle I think. The comment explains the conceptual reason why it's true.

[mathlib-bors]

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

[kbuzzard]

Thanks! I pushed two small golfs, feel free to merge before CI if they look fine to you. (I did test them)

They book look great to me! Thanks!

[kbuzzard]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build