sigma.topological_space

Stream: new members

[Nicolò Cavalleri]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Nicolò Cavalleri]

Adam Topaz said:

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

I am lost, does it refer to the post?

[Adam Topaz]

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

[Adam Topaz]

But it's not clear the projection is continuous

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Nicolò Cavalleri]

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]

Adam Topaz said:

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Nicolò Cavalleri]

Adam Topaz said:

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

Ok I hoped I could find another way but I will do this, thanks!!

[Reid Barton]

Ultimately the best way to do this is probably just the traditional way: write down the total space and put the topology you want on it