Stream: new members

Topic: sigma.topological_space

Nicolò Cavalleri (Oct 17 2020 at 14:46):

If i understand correctly the instance sigma.topological_space gives the sigma type the disjoint union topology. By searching for sigma.topological_space across mathlib it seems this has not been used even though I don't know if it were used after opening the namespace sigma. My question is: why is this natural? If A and B are two topological spaces would it not be more natural to consider the product topology on the constant sigma type? I would need to remove it from mathlib or to add the hypothesis that the base type of the sygma type has the discrete topology. Is it a problem?

Kevin Buzzard (Oct 17 2020 at 14:50):

I'm not sure I completely understand the question but the sigma type instance you're talking about has no assumption that alpha is a topological space, so it is literally just the assertion that if you have a bunch of topological spaces indexed by alpha then their disjoint union naturally has a topological space structure. I don't know what A and B are supposed to denote in your question.

Nicolò Cavalleri (Oct 17 2020 at 14:55):

Oh ok is disjoint union by rule implemented with the sigma type, I mean is there no any kind of type synonim or something? My point is, what if in \Sigma x : \alpha, \beta x, \alpha is not meant to be a type of indices but it is a topological space and I want to give to the sigma type a different topology from the disjoint union, should I just define an instance over that of the disjoint union?

Kevin Buzzard (Oct 17 2020 at 14:59):

I see. If you're stuck with the instance and you don't want it then sure you could use a type alias, the instance would not move over to that by default. I have no idea how this would work though. If alpha has a topology and you want this to be reflected in the sigma type then wouldn't you have to have some concept of what it means for an open subset of beta(x) to be "close to" an open subset of beta(y) if x is close to y? As I'm sure you know, the whole point of the sigma type is that the different beta(x)'s don't have to be related in any way.

Kevin Buzzard (Oct 17 2020 at 15:00):

If you're really just interested in a product of topological spaces, just use the product of topological spaces in mathlib with its product topology.

Adam Topaz (Oct 17 2020 at 15:01):

You can take the coarsest topology where the projection to alpha is continuous, for example...

Kevin Buzzard (Oct 17 2020 at 15:02):

If all the beta(x) were equal then a back of an envelope calculation indicates that this would not give you the product topology (which was mentioned in the original post) but of course you're absolutely right.

Adam Topaz (Oct 17 2020 at 15:02):

You're right, it says nothing about the beta x

Nicolò Cavalleri (Oct 17 2020 at 15:03):

You're right, it says nothing about the beta x

I am lost, does it refer to the post?

Adam Topaz (Oct 17 2020 at 15:03):

You could take the coarsest topology which contains that, and where all the fibres have the right topology

Adam Topaz (Oct 17 2020 at 15:03):

But it's not clear the projection is continuous

Adam Topaz (Oct 17 2020 at 15:04):

I think we're just trying to figure out what topology you want to introduce on this object :smile:

Kevin Buzzard (Oct 17 2020 at 15:04):

yes, we're still trying to understand what A and B are in your question :-)

Adam Topaz (Oct 17 2020 at 15:10):

Is there a way of saying that the spaces beta x vary continuously in x?

Nicolò Cavalleri (Oct 17 2020 at 15:10):

Well yes depending on the specific example you are working with there are many ways to define different topologies than the disjoint union one, and I want to understand how should I deal with the conflict with the sigma.topological_space instance. In my question A and B are just two topological spaces of which I want to consider the product topology on the sigma type, and I do not want to use the product. But this was just an example to illustrate the point, it could be any other thing that like what Adam said, it could be the Moebius bundle, I just want to consider different topologies on the sigma type.

Nicolò Cavalleri (Oct 17 2020 at 15:10):

Is there a way of saying that the spaces beta x vary continuously in x?

Yes in the case of vector bundles for example

Adam Topaz (Oct 17 2020 at 15:11):

Sure any fibre bundle works too, but it assumes you start with a big space and you're looking at the fibres

Adam Topaz (Oct 17 2020 at 15:12):

Note that general topological spaces do not form a Cartesian closed category

Adam Topaz (Oct 17 2020 at 15:15):

If you could define a topology on Top (the type of all topological spaces), this could work in general

Adam Topaz (Oct 17 2020 at 15:18):

Anyway, the practical solution to making new instances on existing types is to define a type synonym.