IsTopologicalModule

Stream: mathlib4

[Kevin Buzzard]

Apparently a topological module over a topological ring is a module such that SMul and Add are continuous. Should we have this concept in mathlib or is it "already there" via [ContinuousSMul R A] [ContinuousAdd A]?

[Yaël Dillies]

If we had it, it couldn't be a typeclass because in the hypothetical instance IsTopologicalModule R A → ContinuousAdd A we have R appearing in an hypothesis and not in the conclusion

[Kevin Buzzard]

Yes I've run into this already :-(

[Johan Commelin]

Right, so A needs to be a TopologicalAddMonoid, which amounts to ContinuousAdd, I suppose. And then TopologicalModule would be an alias for ContinuousSMul

[Edward van de Meent]

presumably TopologicalAddCommMonoid?

[Johan Commelin]

Well, it would be a mixin, at least that is what mathlib currently does to mix algebra and topology.

[Edward van de Meent]

ah yes, i see :thinking: