Zulip Chat Archive

Stream: maths

Topic: pullback ring topology?


view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:20):

Idle question that just came up: if R is a ring, and X is a topological space and f: R -> X is a map, there is certainly a canonical smallest topology on R which makes f continuous -- but is there a smallest topological ring structure on R which makes f continuous? This would not surprise me -- but the details would need checking. Is this some sort of question which Galois insertions or whatever can just answer instantly? Note: a topological ring is a ring and a topology such that + and - and * are continuous maps.

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:22):

We would need to check that structure preserving topologies form a complete lattice, i.e. they are closed under arbitrary intersection

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:22):

that's a math question

view this post on Zulip Adrian Chu (Apr 25 2019 at 07:23):

known*

view this post on Zulip Adrian Chu (Apr 25 2019 at 07:23):

Is the answer to the corresponding question to group known?

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:24):

I've just told you the definition: it's some type R plus some random collection of maps R^n -> R and they all have to be continuous. So it's a model theory question not a maths question.

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:25):

no, I mean is the intersection of a bunch of topologies respecting the operations, a topology respecting the operations?

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:25):

The answer to that question is independent of the operations in question, right?

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:25):

OK so you're saying that it's a question in topology maybe. I want a model theorist to mumble something about second order structures or something, but you want me to do the work.

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:26):

I'm pretty sure if the answer to that is yes then it's true for any algebraic theory

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:26):

so topological groups, rings, etc

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:26):

If I have a bunch of topologies on R then I get a bunch of topologies on R^2. The "union" topology on R induces the "union" topology on R^2. Surely. Someone should check in Lean ;-)

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:27):

And then if f : X -> Y is continuous for a bunch of pairs of topologies on X and Y, then it's surely continuous for the union topology.

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:28):

yeah, sounds plausible

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:28):

Great. So why didn't you guys do this in the topological ring API? We need it ;-)

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:28):

I suppose we'll have to make it ourselves ;-)

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:28):

Basically that means endowing topological_ring A with a complete lattice structure

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:29):

which you can do by galois insertion like you said

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:29):

Maybe it's about time I learnt what a Galois insertion was.

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:29):

I think that's the same way topological_space A gets it's structure, you can look at that

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:33):

Ah, for the galois insertion you need the forgetting map from topological_ring to topological_space, and then it's adjoint (left? right?) that builds that least topological_ring structure finer than the input topological_space

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:33):

Indeed.

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:34):

And I was basically wondering whether this construction is already somehow a trivial special case of some hugely general construction which is already in mathlib somewhere

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:35):

Actually the part about generating a topology on X making a function f : X -> X continuous looks a little suspicious

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:35):

I think it will work, but it's sort of inductive

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:36):

you have one already, right?

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:37):

There are certainly plenty of ways to build topologies, and you can cobble them together to build this, but I don't think making a least topological_ring is a direct application of anything in mathlib

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:38):

Aah so it is not as formal as I had hoped.

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:39):

And in fact if we want X^2 -> X continuous then it's now less clear how this induction is working. "Hey, we want this random subset of X^2 to be continuous -- please put a sensible topology on X which guarantees this"


Last updated: May 12 2021 at 08:14 UTC