What topological spaces do we have?

Stream: general

[Kenny Lau]

I'm aware that this place does not value examples, just abstract theorems, but do we have R^n? C^n? S^n? D^n?

[Kenny Lau]

by "this place" I mean Mario

[Mario Carneiro]

I like examples when they are abstract constructions :)

[Mario Carneiro]

In this case you're talking about making a topological space out of K^n where K is a topological field or vector space

[Kenny Lau]

that's only the first two cases :)

[Mario Carneiro]

For S^n and D^n, I would just define them as the appropriate subspaces. There are loads of more abstract definitions of S^n of course, but I would suggest sticking to actual spheres for the definition

[Kenny Lau]

agreed, but do you have norm?

[Mario Carneiro]

Patrick had a working definition

[Kenny Lau]

in R^n?

[Mario Carneiro]

Hm, it occurs to me that "the unit sphere" is well defined in any normed vector space

[Kenny Lau]

for god's sake

[Mario Carneiro]

Patrick's definition gives a norm on any normed space

[Mario Carneiro]

of course R^n will be a normed space

[Mario Carneiro]

but there is some concern about whether to use the 2-norm vs some other p-norm

[Mario Carneiro]

If you just need something quick and dirty for some application, go ahead and define it however you like

[Kenny Lau]

I don’t need it now

[Mario Carneiro]

The simplest abstract definition if you only need the topological structure is by iterating the suspension operation on bool

[Kenny Lau]

good luck proving that S^n \ {pt} ~ R^n

[Kenny Lau]

good luck finding a single point inside

[Mario Carneiro]

I guess it's not obvious that S^n is homogeneous as the suspension, but it's easy to show S^n \ {north pole} ~ R^n

[Kenny Lau]

hmm

[Kenny Lau]

and R^n \ {0} def retracts to S^(n-1)?

[Mario Carneiro]

That's dead easy with the suspension, since R^n\{0} maps to S^(n-1) x (0,1)

[Kenny Lau]

tu ganhas

[Mario Carneiro]

I agree that homogeneity is easier with the geometric representation, since then you can use orthogonal transformations

[Kenny Lau]

next time someone asks me what S^n is, I’m gonna say “repeated suspension of bool” :stuck_out_tongue:

[Kenny Lau]

they be like “entao o que e bool?”

[Mario Carneiro]

I think that's the definition the HoTT people use, more or less

[Mario Carneiro]

Also, if you do repeated suspension on unit you get D^n

[Mario Carneiro]

or just take [0,1]^n

[Mario Carneiro]

But for a mathlib definition, I would imagine it will be used in many contexts, not just topological, i.e. you might care about manifold structure in which case "corners" are not appreciated

[Patrick Massot]

I almost have $\mathbb{R}^n$ as a topological space. I only need to find one day without a million urgent things to do. I have normed spaces and Pi instances for many things. But indeed the norm we'll have on $\mathbb{R}^n$ will have box balls, which is not good if you want to get a smooth $\mathbb{S}^{n-1}$.

[Kenny Lau]

https://math.stackexchange.com/a/2712786/328173

[Kenny Lau]

@Mario Carneiro this is part of the reason I asked that question

[Kenny Lau]

if we have enough lemmas we might be able to formalize that