Partial homeomorphism of open cells in a CW complex

Stream: maths

[Robert Maxton]

So, my project to prove equivalence of docs#Topology.RelCWComplex and docs#TopCat.RelativeCWComplex is unfortunately nowhere near as close to complete as I had hoped. docs#Topology.RelCWComplex requires, for each $n$-cell of the complex, a docs#PartialEquiv between the (open) unit $n$-ball $\mathbb{B}^n$ and the corresponding open cell, whose forward direction is continuous on the entirety of the closed unit $n$-ball $\mathbb{D}^n$ and whose reverse direction is continuous on the open cell.

Using categorical properties of Top and the abstract RelativeCWComplex, I've managed to prove that the relevant maps are all injective on $\mathbb{B}^n$, thus each define a PartialEquiv, and that they are continuous on $\mathbb{D}^n$. However, I'm stuck on showing that the reverse direction is continuous. Essentially, the issue is that I'm caught between two complications:

• On the one hand, the reverse direction of this partial equiv isn't concretely defined, it's just a noncomputable partial inverse given by choice. That makes it hard to directly prove things about the inverse; instead, I've been trying to generate a PartialHomeomorphism by a similar noncomputable approach. I believe -- though #xy is always a concern -- that this requires me to show that the forward map is an open embedding when restricted to $\mathbb{B}^n$.
• On the other hand, the relevant maps are given as being out of $\mathbb{D}^n$, and since (I think) $\mathbb{D}^n$ is unfortunately not coherent with $\left\{\mathbb{B}^n, \mathbb{S}^{n-1}\right\}$, most of the obvious ways to convert the map into a hom out of $\mathbb{B}^n$ break the colimiting properties I need to prove anything useful about them categorically.

... Writing this out has given me an idea, but I'm going to post this anyway, in the hopes that I might get a better one from the community. The question is: what's the best way to show that the maps 𝔹 n ⟶ openCell n _ are partial homeomorphisms, or more specifically open maps, within a categorical setting and starting with primarily categorical data?

[Michael Rothgang]

(If you use $$double dollars$$, the LaTeX will come out correctly.)

[Joël Riou]

In https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/TopCat/ClosedEmbeddings.lean (and neighbouring files), I show some properties which may be relevant. In particular, closed embeddings are stable by pushouts, which may be applied here at each step in the inductive system which defines a CW-complex. Roughly speaking, when we add a n-cell, we are doing a pushout of the inclusion of the boundary in a ball (which is a closed embedding), the resulting map is also a closed embedding, so that the complement is open: using the characterization of open subsets in a colimit, it should not be too hard to show that the open ball actually identifies as an open subset in the pushout.

[Hannah Scholz]

I am not sure if I understand correctly what you are doing but if I do then here a quick comment: While I don't know how to fix your issue, there is one problem I see with your approach. The PartialEquivs needed in docs#Topology.RelCWComplex are in general not open maps. In fact, the image of the open ball isn't open in general for dimensional reasons (think of the construction on the sphere with two cells in every dimension). So you won't be able to use a PartialHomeomorph is think. What @Joël Riou has said is still correct, they are open in their respective skeleton. So you probably could define your map as a composite of two maps: one mapping to the skeleton, which then should be an open embedding, and then the second one going from the skeleton to the whole complex, where continuity properties are hopefully easier to show.

[Robert Maxton]

@Hannah Scholz Good point, thank you. Yes, I should definitely be splitting this problem in two.
@Joël Riou Hmmm. I'd chased a route like that before, but got hung up on _where_ I was taking the complement; in order to create an open embedding into the $n$-skeleton, I would naturally be taking the complement of the image of the sphere in the $n$-skeleton, and that includes both the interior of that open cell and everything outside it, and I would need to prove that 'everything else' is closed.

... I believe it is in fact true that each $n$-skeleton is closed (in both the complex and the next skeleton), and similarly each individual closed cell, so perhaps this does count as a reduction of the problem. I'll have to think about where to go from there. Thanks for the tip, at any rate!

[Joël Riou]

Well, I have considered the pushout diagram corresponding to attaching one n-cell for simplicity, but one may also consider the pushout diagram which relates the n-skeleton and the n+1-skeleton. As closed embeddings are stable under coproducts, pushouts and transfinite compositions (which is proved in the file I linked to), the n-skeleton is closed in the n+1-skeleton, and in the whole space.

[Robert Maxton]

@Joël Riou Actually, wait, now I remember the obstacle: AFAICT the closed cells aren't embeddings at all, because they aren't necessarily injective! The maps are only injective on the open cells, the boundaries can even be mapped to a single point.

[Robert Maxton]

Which I guess I should probably list as a third important complication: only the open cells are in fact 'embedded', but all my nice categorical properties are stated in terms of the closed cells and the closed disk.

[Robert Maxton]

So... I probably need to split up my function properties; show that the open cells are embeddings, and seperately show that they're open maps, at least in their skeleton.

[Joël Riou]

What I have been trying to say is that in order to understand the topology of CW-complexes (from the categorical definition), you need to understand the topology of certain pushouts (and also of colimits indexed by ℕ), in particular pushouts squares where the left map is a closed embedding (e.g. the inclusion of the boundary of the closed ball, or a coproduct of copies of this map).

[Robert Maxton]

Sure. I've got about 4,000 lines of miscellaneous helper results on the topic at this point >.>;

The problem is that, as far as I can tell, those results don't actually directly apply to the thing I'm trying to prove, because the specific pushout we're taking in fact removes the property I'm trying to prove, and adjusting the comm. sq. so that the property is preserved breaks its pushout-ness.

In this case, having borrowed a few files from TopCatModelCategory, I can prove that the map from one skeleton to its successor is a closed embedding, but pulling back that map to any specific closed cell breaks that proof in multiple ways.

[Robert Maxton]

Again, I know that I can't possibly prove that each map 𝔻 n ⟶ skeleton (n + 1) representing a closed cell is a closed embedding, because it simply isn't true; that map is allowed to send all of ∂𝔻 n to a single point, for example. It is true that the maps 𝔹 n ⟶ skeleton (n + 1) representing open cells are open embeddings, but I don't see how to derive that from categorical data.

[Robert Maxton]

At the moment, I'm building up the theory of regular categories, since $\mathbf{Top}^\mathrm{op}$ is regular and regular monos in Top are precisely topological embeddings

[Joël Riou]

For simplicity, assume that we add only one n-cell: the map sk n ⟶ sk (n + 1) (whatever the numbering is) is the pushout of the inclusion of the sphere in the closed ball. As a pushout of another map, sk n ⟶ sk (n + 1) keeps certain properties that I have mentionned before: it is a closed embedding. As the forget functor from TopCat to Type preserves colimits, we also have a pushout square in types. From the study of pushout squares in the category of types (when the left map is injective), it follows that the complement of the sphere in the closed ball, i.e. the open ball, injects in sk (n + 1): let us denote B this subset of sk (n + 1). (Set theoretically, sk (n + 1) is the disjoint union of sk n and B.) Because sk (n + 1) is a pushout, a subset of sk (n + 1) is open iff both its inverse images to sk n and to the closed ball are open. It follows that B is open in sk (n + 1).

[Robert Maxton]

Sure, I agree with that much. But that only knocks out two out of three requirements: it's injective, the image is open, but how can we show that it's an embedding? AFAICT, the above proof of openness relies on the fact that the set being considered is the entire image; if it works with arbitrary sets, I don't see it

[Robert Maxton]

Regardless, thanks for the tip, as I hadn't really come up with a concrete plan for getting the open-image-ness yet; I've at least implemented the above in Lean now

[Ruben Van de Velde]

What's an embedding to you if not an injective function?

[Robert Maxton]

A topological embedding, in this context; a function that is both injective, and a witness that the topology on its domain is precisely that induced by the function from the topology on its codomain
i.e. docs#Topology.IsEmbedding

[Joël Riou]

Showing the topology is induced is not more difficult than showing it is open.

[Joël Riou]

Robert Maxton said:

AFAICT, the above proof of openness relies on the fact that the set being considered is the entire image; if it works with arbitrary sets, I don't see it

I have no idea what "set" you are talking about.

[Robert Maxton]

To prove a function is inducing, one must show that every open set in the domain is the preimage of an open set in the codomain. We have proven that the range is open, but now we must extend that proof to every open set

[Robert Maxton]

Anyway, if it really is the same proof, then all the more so I think I should go work on regular categories now, because regular categories are used to define coherent categories and only in a coherent categories can you meaningfully define a 'complementation' operation categorically on subobjects

[Robert Maxton]

And much of the complexity of my current implementation of the above proof comes from having to move between set-theoretical and categorical notions, as the proof relies heavily on ∂𝔻 and 𝔹 being complements