# Zulip Chat Archive

## Stream: maths

### Topic: pullback ring topology?

#### 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.

#### 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

#### Mario Carneiro (Apr 25 2019 at 07:22):

that's a math question

#### Adrian Chu (Apr 25 2019 at 07:23):

known*

#### Adrian Chu (Apr 25 2019 at 07:23):

Is the answer to the corresponding question to group known?

#### 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.

#### 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?

#### Kevin Buzzard (Apr 25 2019 at 07:25):

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

#### 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.

#### 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

#### Mario Carneiro (Apr 25 2019 at 07:26):

so topological groups, rings, etc

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

#### 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.

#### Mario Carneiro (Apr 25 2019 at 07:28):

yeah, sounds plausible

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

#### Kevin Buzzard (Apr 25 2019 at 07:28):

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

#### Mario Carneiro (Apr 25 2019 at 07:28):

Basically that means endowing `topological_ring A`

with a complete lattice structure

#### Mario Carneiro (Apr 25 2019 at 07:29):

which you can do by galois insertion like you said

#### Kevin Buzzard (Apr 25 2019 at 07:29):

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

#### 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

#### 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

#### Kevin Buzzard (Apr 25 2019 at 07:33):

Indeed.

#### 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

#### 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

#### Mario Carneiro (Apr 25 2019 at 07:35):

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

#### Kevin Buzzard (Apr 25 2019 at 07:36):

you have one already, right?

#### 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

#### Kevin Buzzard (Apr 25 2019 at 07:38):

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

#### 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