Continuous map from unit sphere to unit box

Stream: Is there code for X?

[Robert Maxton]

What's the nicest existing way to come up with a continuous map from the unit sphere (i.e. the sphere in $n$-dimensional Euclidean space) and the unit box (i.e. the sphere in Fin n → ℝ by the uniform/maximum metric)? Is there a better way than docs#exists_homeomorph_image_interior_closure_frontier_eq_unitBall ?

[Jireh Loreaux]

I think you should just use docs#guageRescale directly.

[Jireh Loreaux]

you can add a version of docs#image_gaugeRescaleHomeomorph_closure about docs#frontier.

[Robert Maxton]

Hm. Well, alright. I'm not very familiar with that part of the library so I was hoping there'd be a prewrapped version for me to use, but if not I'll figure it out. Thanks for the pointers~

[Jireh Loreaux]

Prewrapped in what way? Which part of that declaration seems hard to use? (I'm asking because I can give you some pointers)

[Jireh Loreaux]

Wait, do you only want continuity?

[Robert Maxton]

Ah, well. I don't know what a Bornology is, is my first problem.

[Jireh Loreaux]

Perhaps what you're looking for is docs#PiLp.continuousLinearEquiv ? (probably it's not strong enough for what you need)

[Jireh Loreaux]

You don't really need to know what a bornology is. You just need docs#NormedSpace.isVonNBounded_ball for one of the sets and something like docs#NormedSpace.isBounded_iff_subset_smul_ball for the other one.

[Robert Maxton]

Ooh. That'll do nicely.

Yeah, I'm trying to prove that docs#Topology.RelCWComplex and docs#TopCat.RelativeCWComplex are in fact equivalent, but the former uses the uniform metric for its 'spheres' and the latter uses Euclidean spheres. So yes, I'm pretty sure all I actually need is a continuous map I can precompose the cell maps with, though a homeomorphism would be nice.

[Robert Maxton]

So, yeah, docs#gaugeRescaleHomeomorph + the existing lemmas ball lemmas to make a frontier version is probably what i want. Thanks!

[Junyan Xu]

the former uses the uniform metric for its 'spheres'

I think this is unintended and we should just change to Euclidean spheres.

[Robert Maxton]

I mean, it's certainly intended, there's a doc-comment that explicitly mentions it

[Robert Maxton]

It'd be reasonable to just change it, though