On IsModuleTopology

Stream: maths

[Johan Commelin]

Branching into a new topic

Kevin Buzzard said:

In particular IsModuleTopology.of_continuous_isOpenMap_algebraMap ...

I can't find that in Mathlib. Is it something in FLT? (Edit: it's in FLT, and Kevin even mentioned that in the same sentence. I should read more slowly :man_facepalming:)

Because it sounds very related to something I was discussing with @Yakov Pechersky concerning #24627

[Johan Commelin]

Concretely, Yakov is formalizing statements about rings of integers that mix topology and algebra. And I encouraged him to try to avoid talking about $\mathcal{O}_K$ in favour of a setup that avoids the precise defeq of the ring of integers.

[Johan Commelin]

As Yakov then told me:

We would then need to install IsModuleTopology on the relevant constructions, like Z_p/Q_p etc

There's also a TODO about IsLinearTopology and ModuleFilterBasis, I tried writing a proof saying one implies the existence of the other under a compatible topology but got stuck.

It seems like we have many slightly different ways of linking topology with a module structure.

[Johan Commelin]

So I'm interested in thoughts/reviews/hints from people familiar with IsModuleTopology.

cc @Kevin Buzzard @Stepan Nesterov

[Anatole Dedecker]

I'm not sure how relevant that is, but mathematically, IsModuleTopology is way stronger than a "compatibility" condition. It should really be called IsFinestModuleTopology.

[Anatole Dedecker]

The reason this name is especially problematic is because what is usually called a "topological module" is simply {R M : Type*} [Ring R] [AddCommGroup M] [TopologicalSpace R] [TopologicalSpace M] [IsTopologicalRing R] [IsTopologicalAddGroup M] [ContinuousSMul R M]

[Anatole Dedecker]

IsLinearTopology corresponds to SubmodulesBasis, rather than ModuleFilterBasis.

[Kevin Buzzard]

Yes, moduleTopology is a lousy name. One of the motivations for me to ask the MO question was to discover what the "actual name" of this topology is. Of course we could go for sawinTopology! I would be happy to change everything to finestModuleTopology and IsFinestModuleTopology.

[Kevin Buzzard]

One thing I'm absolutely convinced by is that it is a useful concept, at least for formalization purposes. It is a beautiful definition and has many nice properties.

[Yakov Pechersky]

I still have a question stemming from Johan's initial inquiry: if I have IsLinearTopology R R, what is the correct setting to infer IsLinearTopology R Frac(R) or IsLinearTopology R K for IsFractionRing R K? What kind of relationships do we have between a topological space R and its fraction ring K -- do we have anything that relates the two topologies in the relevant way other than ContinuousSMul R M?

[Ben Eltschig]

Kevin Buzzard said:

Yes, moduleTopology is a lousy name. One of the motivations for me to ask the MO question was to discover what the "actual name" of this topology is. Of course we could go for sawinTopology! I would be happy to change everything to finestModuleTopology and IsFinestModuleTopology.

I don't remember if I've said this before, but in the context of diffeology and vector spaces the corresponding diffeology is usually just called "the fine diffeology" on a given vector space. So I think calling it "the fine module topology" makes sense here, though of course "finest" is probably an even better descriptor.

[Kevin Buzzard]

Then I think I prefer "fine" to "finest".

[Antoine Chambert-Loir]

Note that there is something called the “fine topology” in potential theory.