Action topology

Stream: Is there code for X?

[Kevin Buzzard]

Do we have either of these already? Do we want them?

import Mathlib.Topology.Order
import Mathlib.Algebra.Group.Action.Defs

class IsActionTopology (R M : Type*) [SMul R M]
    [TopologicalSpace R] [TopologicalSpace M] : Prop where
  isActionTopology : (inferInstance : TopologicalSpace M) =
    ⨆ m, .coinduced (· • m) (inferInstance : TopologicalSpace R)

def ActionTopology (R M : Type*) [SMul R M] [TopologicalSpace R] :
    TopologicalSpace M := ⨆ m, .coinduced (· • m) (inferInstance : TopologicalSpace R)

I want to use the class to express that a topology on a finite free R-algebra is the product topology once you pick a basis (which I don't want to pick), and there was an interesting discussion I think in #maths but which I can no longer find due to incompetence, but once Adam pointed out the correct definition I realised when beginning to think about it that it all just works for SMul with no addition or multiplication needed anywhere. I think this abstraction will make some development of the theory of adelic quaternion algebras easier. For example I think one can prove that if D is a finite free R-algebra then the action topology is a ring topology (this is ongoing work of some students).

[Yaël Dillies]

So this is sort of the "equality version" of ContinuousSMul where ContinuousSMul is the "≤ version"?

[Yury G. Kudryashov]

It's the equality version of the non-existing ContinuousSMulConst.

[Yury G. Kudryashov]

I don't know if it implies ContinuousSMul.

[Yaël Dillies]

Oh, it's different from docs#ContinuousConstSMul

[Yury G. Kudryashov]

Yes. AFAICT, we don't have examples of actions that

• someone cares about;
• have ContinuousSMulConst property;
• have no ContinuousSMul property.
  If I'm wrong, then we should add a ContinuousSMulConst typeclass.

[Kevin Buzzard]

I am in a situation where I have an algebra which is free of rank 4 over a base topological ring, and I want to just put a topology on it which will be the product topology if I were to choose a basis, and then show that this topology makes the algebra into a topological ring. I propose doing this by either putting an arbitrary topology on the algebra and then adding the typeclass that it's the action topology, or defining the action topology on it directly. Either way I then want a theorem telling me that multiplication is continuous and hence that it's a topological ring (which I think I can probably prove just from the definition of the action topology in the finite free case, but it seems to be slightly delicate and the students haven't finished yet).

[Kevin Buzzard]

However I am certain in this case that ContinuousSMul will be true. The difference between ContinuousSMul and what I'm doing is that I'm defining the topology on the space being acted upon using only the topology on the space which is acting. I am not sure that it's possible to say "given [SMul G X] and a topology on G, take the coarsest/finest topology on X such that ContinuousSMul G X is true".

[Yury G. Kudryashov]

See docs#continuousSMul_sInf

[Yury G. Kudryashov]

However, I'm not sure that sInf {t | @ContinuousSMul G X _ t} is your topology (which requires ContinuousSMulConst only).

[Kevin Buzzard]

I see, so maybe the action topology should be the smallest topology making the action continuous?

All I want at the end of the day is that if R is a topological ring then for a space isomorphic to R^n as space-with-action, the automatically generated topology is equal to the product topology. Is this true for the sInf I wonder?

[Yaël Dillies]

I am suspicious that you might need to add terms of the form .coinduced (r • ·) to your infimum

[Kevin Buzzard]

Over the last few days I've got a much better understanding of these two proposed definitions of an induced topology. The set-up: $R$ has a topology and $R$ acts on $A$ and we want a topology on $A$. We have the definition ⨆ m, .coinduced (· • m) (inferInstance : TopologicalSpace R) originally posted above (the "action topology"), and sInf {t | @ContinuousSMul G X _ t} (the "sInf topology"). This post is simply a summary of what I know right now, and what I'll be doing next.

My motivation for this construction was that I wanted to get some proofs for free. Here's an example of something I want to do. Let $R$ be a commutative topological ring and let $A$ be a (not necessarily commutative) $R$-algebra which is finite and free as an $R$-module. I want to say "Put the obvious topology on $A$ and now it's obviously a topological ring". How might one start this in Lean? Well at the minute it's "pick an R-basis of A, now use the product topology, now worry about why this doesn't depend on the choice of basis, now prove that multiplication on A is continuous because matrix multiplication is continuous". I felt that this proof could do with some abstraction, so I started looking for "magic" topologies on A just coming from the fact that R acts on A, and then the idea was to prove nice facts about these topologies.

Unfortunately, of the three topologies I've tried so far, the two discussed above do not give the answer I want for A=R^2 :-(

Because I've just figured it out, I may as well write things down here. Note: I didn't formalise much of the below so there might be mistakes. However I did try and fail to prove that if $R=\R$ and $$A=\C$$ then we get the product topology and I'm pretty convinced that this is now false.

With the ActionTopology I suggested above, the induced topology on $\mathbb C$ is the smallest one making all the $\R$-linear maps $\R\to\mathbb C$ continuous, so a subset of $\mathbb C$ is open iff its intersection with every line through the origin is open if you identify the line with $\R$ in a sensible way. In particular sets like $\{(x,x):1<x<2\}$ are open for this topology :-( One can check (I didn't formalise this) that the action of $\R$ on $\mathbb C$ is continuous if both $\mathbb C$'s are given this topology, and so by definition of sInf {t | @ContinuousSMul G X _ t} the sInf topology is <= the action topology, and in particular $\{(x,x):1<x<2\}$ is also open for the sInf topology as well.

The topology which works for me turns out to be the one where we make all $R$-linear maps $A\to R$ continuous. This doesn't just work now for SMul, you need Monoid R and [ContinuousMul R] for this to even make sense. But @Ludwig Monnerjahn and @Hannah Scholz proved that with this topology, you do get the product topology, and for algebras which are finite free R-modules you get that multiplication is continuous for free. See here for Lean proofs.

Hannah and Ludwig -- I didn't like your topology at the time because I preferred the ideas in this thread, but now I've realised that the ideas in this thread don't work! So I'm going back to your work (actually I'm going on holiday, but in 2 weeks' time I'll be going back to your work). I started tidying it up here.

[Adam Topaz]

@Kevin Buzzard another approach that might be worth trying is to look at all linear map $R^n \to A$ with $n$ a natural, and take the supremum over the coinduced topologies of those. I'm quite sure this would at least give a good topology in the case of flat modules.

[Kevin Buzzard]

You keep derailing things by suggesting more topologies!! I'm trying to get some work done here!

Actually this one sounds really promising. The problem with just doing maps R -> A is, well, if you read what happens for the complexes above then I suspect you can see the problem already. If you ask that all maps C -> R are continuous then this stops that weird open line interval being open, but your trick of using R^2 will also do that.

[Adam Topaz]

Sorry Kevin! :-/

[Kevin Buzzard]

No it's great, I've sunk a lot of work into understanding the three topologies which one gets on a module over a topological ring and so I may as well understand this one too, to see how it fits into the picture. My initial instinct is that this is the right one for the application (but then again that was my initial instinct with the other three topologies -- however I understand the problem much better now I've had a few days to actually do some mathematics, something which is vanishingly rare in my life nowadays but roll on October...)

[Kevin Buzzard]

OK so I've not formalised everything, but I think that this new topology suggested by Adam is the best one yet.

The set-up: $R$ is a topological ring and $A$ is an $R$-module. Then $A$ inherits a "natural topology" (I'm just picking a random adjective to distinguish it from all the other topologies introduced here) from $R$, and it's the smallest topology making all $R$-linear maps $R^n\to A$ continuous. The theorems: the given topology on $R$ is natural, the product topology on $R^n$ is natural, any $R$-linear maps $M\to N$ is continuous for the natural topologies, if $R^n\to M$ is surjective then the natural topology on $M$ is the pushforward of the product topology (all formalised), and I hope that if $M$ is f.g. then addition is commutative for the natural topology (and this is fine if M is f.g. free, which is true in my application). Next I want to prove that if $R$ is furthermore commutative and $A$ is an $R$-algebra which is f.g. as $R$-module (or possibly f.g. and free) then the multiplication on $A$ is continuous for the natural topology and thus $A$ is a topological ring. This will be enough for my purposes, and I suspect it's true.

[Kevin Buzzard]

NB here's a wrong turn you can go down: just let $R$ be a topological monoid. Then the definition still makes sense, but it doesn't look so powerful: e.g. you can't "write down a formula" for a general $R$-linear map $R^2\to R$. To see this, imagine the case when $R=G$ is a group. Then maps $\phi:G^2\to G$ satisfying $\phi(g(h,k))=g\phi(h,k)$ are not determined by their values on two elements, you need to know the values of $\phi(1,k)$ for all $k$, so $G^2$ feels very much like a disjoint union of $|G|$ copies of $G$ here. The moment you have a topological ring you can also ask that $\phi$ preserves addition and that addition is continuous, and these are key to get the theory going.

[Kevin Buzzard]

tl/dr: if $R$ is a topological ring then all f.g. $R$-modules (or possibly only f.g. free ones) inherit a "canonical" topology with nice properties. Does this topology have a name?

[David Michael Roberts]

The topology suggested by Adam feel analogous to how a compactly-generated topology can be characterised. Just as it can be the final topology for the collection of all continuous maps from compact Hausdorff spaces, one can say the topology is from a single map out of the coproduct indexed by the set of all such maps (or rather, blah blah kappa-compactly generated etc etc, to make sure it's not a proper class).

Then this linear topology feels like it should be the same as that induced as a quotient from the direct sum over finite-gen free modules, indexed by all linear maps to the module, taking the colimit topology on the direct sum, and the product topology on the fin.free modules. Then just as in the compactly-generated topology case, one can cut the giant coproduct/direct sum down to a smaller one that is indexed by a 'sufficiently large' set of maps. Characterising what 'sufficiently large' looks like then feels like it can be flexible enough to prove the stability properties etc that are needed.