pullback ring topology?

Stream: maths

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

that's a math question

[Adrian Chu]

known*

[Adrian Chu]

Is the answer to the corresponding question to group known?

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

so topological groups, rings, etc

[Kevin Buzzard]

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 ;-)

[Kevin Buzzard]

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.

[Mario Carneiro]

yeah, sounds plausible

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

Basically that means endowing topological_ring A with a complete lattice structure

[Mario Carneiro]

which you can do by galois insertion like you said

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Indeed.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

you have one already, right?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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"