RelCWComplex design

Stream: mathlib4

[Robert Maxton]

@Hannah Scholz @Floris van Doorn So, I'm approaching the conclusion of a project to prove the equivalence of docs#Topology.RelCWComplex and docs#TopCat.RelativeCWComplex . At the very last step, though, I've tripped over a bit of strange design in docs#TopCat.RelCWComplex.map .

Specifically, the sources are set to be the (open) docs#Metric.ball , but the complex in fact depends on the behavior of the maps on the boundary docs#Metric.sphere . The fact that the maps are required to be continuous on the entirety of docs#Metric.closedBall is sufficient to complete the definition, which is a neat topology trick, but complicates matters when trying to come up with the gluing maps; it means I can't use docs#PartialEquiv.IsImage.restr to just instantly have the right function, for example. It's not like I can't just use docs#Set.restrict and whatnot instead, but I thought I'd ask if you're actually getting something from that extra bit of slack.

[Floris van Doorn]

What alternative do you propose? AFAIK this is required for the definition. I guess you could alternatively require ∀ x ∈ sphere 0 1, ∃ c, Tendsto (map n i) (𝓝[ball 0 1] x) (𝓝 c), so that the condition only depends on the values of map inside the ball, but that seems strictly more inconvenient to work with.

[Robert Maxton]

... Wait, really? What breaks if you just say source_eq (n : ℕ) (i : cell n) : (map n i).source = closedBall 0 1 ?

[Robert Maxton]

... I mean, I can just go try it. goes to check

[Floris van Doorn]

This was actually a mistaken definition we had before. The problem is that we do not want to require that map is injective on sphere 0 1.

[Robert Maxton]

Huh, really?

Nothing explicitly breaks if I make that change in my copy, at least in Mathlib/Topology/CWComplex/Classical/Basic.lean itself. But I don't know if we have enough API around it to see a subtler flaw.

[Floris van Doorn]

Nothing will break, but you will lose some (constructions of) CW-complexes. For example, make the n-sphere as a CW-complex with 1 point and 1 n-cell. Can you do that with your new definition?

[Robert Maxton]

... I wasn't aware that was possible at all; I thought the construction of the n-sphere required two cells of every dimension from 0 to n-1 ^.^;

[Robert Maxton]

Oh, wait, maybe I see how to do it

[Robert Maxton]

... Ah, okay. Yes, I see now.

[Floris van Doorn]

Note: Hannah defined the n-sphere with 2-cells here: https://github.com/scholzhannah/CWComplexes/blob/master/CWcomplexes/Examples.lean#L643-L649. With 2n+2 cells it's defined here: https://github.com/scholzhannah/CWComplexes/blob/master/CWcomplexes/Examples.lean#L1163-L1166

[Floris van Doorn]

(both definitions need to be polished before we PR them to Mathlib)

[Robert Maxton]

Mmm. Okay, yeah, I see the problem. Sorry to bother you. I guess I'll go bundle up docs#Set.MapsTo after all.

While I have your attention, is there something similarly important underlying the choice of the sup metric for our "spheres"? The lemma providing the homeomorphism between $L^\infty$ spheres and $L^2$ spheres takes up a solid hundred lines... though I do not claim to be an expert in either measure theory or golfing.

[Floris van Doorn]

It might be useful to get a def that turns a partial equivalence with the condition ∀ x ∈ sphere 0 1, ∃ c, Tendsto (map n i) (𝓝[ball 0 1] x) (𝓝 c) into a partial equivalence that is required for CW-complexes (without changing the values inside the ball).

[Floris van Doorn]

About which norm to use, I wasn't super confident. I expected that it was easier to work with cubes than with balls when constructing explicit examples of CW-complexes, but I don't feel strongly about that part of the definition. @Hannah Scholz we did talk about this before. Do you think the library is overall simpler by using cubes instead of balls?

[Hannah Scholz]

For all abstract work I don't think it matters at all. The only place where it is actually noticable is the examples. Since I primarily focused on spheres, I too had to pass through the homeomorphism @Robert Maxton mentions. In the end, since you want the sphere to be a CW complex under all norms, you will need such a map anyways, but I do think it would probably be cleaner to work with spheres instead of cubes from the get-go. For now I have preferred our current solution since its shorter to write but that probably isn't a very good reason. Refactoring what is already in mathlib should be very easy and I can get to that soon if it is wanted.

[Floris van Doorn]

Ok, in that case we want to consider transferring to the standard definition using balls instead of cubes, but I don't think it's super urgent.

[Robert Maxton]

I may just include it in my PR, then, if refactoring Finite won't be too bad?

[Floris van Doorn]

Sounds good to me.