Discrete spaces are CW complexes

[felixpernegger]

This may be a good moment to discuss if we want a standard grammar/terminology for these constructions.

[GeoffreySangston]

Is it common parlance to name the filtration the CW structure? I'm wondering if we have (or haven't) made an unconventional choice here.

Note: A CW-structure on a topological space $X$ is a filtration $X_{-1}\subseteq X_0\subseteq X_1 \subseteq\dots$ satisfying the conditions above.

[felixpernegger]

https://www.math.ru.nl/~gutierrez/files/homology/Lecture08.pdf
This calls the filtration explicitly CW decomposition

Hatcher uses CW structure (not precisely defined) and it seems like he includes the attaching maps when he uses the term

Not sure

[prabau]

Encyclopedia of Gen Top p. 472 also uses "CW-structure" to mean the filtration, i.e., "an increasing sequence of closed subspaces ... which satisfy the following conditions: (i) ... (ii) ... (iii) ..."
(the attaching maps are not part of the CW-structure, but of course their existence is part of the conditions)

[prabau]

T889: the justification is unnecessarily formal. No need for that complication.
It's an obvious result; would be even more so if we had started the construction of a CW complex in the definition with $X_0$ = any discrete space. So we should just claim it. Maybe something like:

A discrete space is a CW complex where all the points are $0$-cells and there are no higher dimensional cells.

or something similarly straightforward.

[felixpernegger]

@prabau are you happy with the proof? It looks good to me.

[prabau]

Not exactly. Although what you have can be understood, I will repeat my comment above #1766 (comment) that it seems overly formal. No need to even mention filtration, etc. My suggestion in that comment seems a lot more straightforward.

And by the way, Felix, weren't you the one advocating in the discussion yesterday that there was not always the need to be so formal? I think that applies here.

@GeoffreySangston care to comment?

[felixpernegger]

Not exactly. Although what you have can be understood, I will repeat my comment above #1766 (comment) that it seems overly formal. No need to even mention filtration, etc. My suggestion in that comment seems a lot more straightforward.

The proof we have now (6 words...) is an exact application of the definition and in now way overly complicated in my opinion.

And by the way, Felix, weren't you the one advocating in the discussion yesterday that there was not always the need to be so formal? I think that applies here.

Not really. It is good to be formal and precise, but one might want to reconsider if this makes the statement overly involved (which is not the case here) and shouldnt waste to much time on trivial details.

[felixpernegger]

Indeed the fact that X0 is discrete is technically not even part of the definition, but a consequence of it

[GeoffreySangston]

@prabau @felixpernegger I don't know if what we've got is too formal or what's meant by that, so sorry if I'm missing the point here. Since there is a construction (though it's uniquely determined), I suppose "By definition." and its variants are not appropriate. I would have thought stating the construction and then letting the reader see that it is clear by definition is a good pi-base proof, assuming our definition makes it clear.

That being said, I feel like the part explaining that the $0$-skeleton is discrete does not pop out enough on the page. It's not part of the definition technically, but maybe it "morally" is? It seems like a bit of quirk that it's not a part of the definition to me, rather than a genuine proposition about CW complexes. What if we change the "definition block" of the property page to:

$X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subseteq \dots$, such that:

• $X_n$ is obtained from $X_{n-1}$ by attaching $n$-cells.
• $X = \bigcup_{n\geq 0} X_n$ and a subspace $U \subseteq X$ is open iff $U \cap X_n$ open in $X_n$ for all $n \geq -1$.
• The $0$-skeleton $X_0$ has the discrete topology; this is a consequence of the definition of attaching $n$-cells given below.

Here attaching $n$-cells means that there is a discrete space $J$, and for every $j \in J$ a continuous map $f_j:\partial D^n \to X_{n-1}$, such that $X_n$ is homeomorphic to the quotient $(X_{n-1} \sqcup (J \times D^n)) /{\sim}$,
where $\sim$ is the equivalence relation generated by $(j,x) \sim f_j(x)$ for all $(j,x)\in J \times \partial D^n$.
The set $J$ is allowed to be empty, in which case $X_n=X_{n-1}$.
If the $0$-skeleton is empty, then $X$ itself is empty.

The exact wording could be reworked.

[prabau]

@GeoffreySangston Yes, such a rephrase would be good. I would even rephrase it in the following way, to match what is in Envycl. of Gen Top, and multiple other sources. Namely, in this order:
(i) $X^0$ is a discrete space, (ii) stuff about attaching n-cells, (ii) X = union of the chain, plus direct limit stuff (weak topology)
And then in a separate comment afterwards we can note that $X_0$ can also be viewed at attaching 0-cells to an empty space.

In addition, we could mention somewhere that the sequence of n-skeletons can be either finite or infinite. And the third condition is only needed if it's an infinite sequence. That's the idea.

Then the fact that a discrete space is a CW complex will indeed become a triviality. And the whole thing will also be slightly more accessible to people who have never seen the notion of CW complex.

If you both agree, I could do an edit as part of this PR. Or you can do one, and we'll go back and forth until we get a good formulation.

[felixpernegger]

@GeoffreySangston Yes, such a rephrase would be good. I would even rephrase it in the following way, to match what is in Envycl. of Gen Top, and multiple other sources. Namely, in this order: (i) X 0 is a discrete space, (ii) stuff about attaching n-cells, (ii) X = union of the chain, plus direct limit stuff (weak topology) And then in a separate comment afterwards we can note that X 0 can also be viewed at attaching 0-cells to an empty space.

I am against this. It doesnt generalise to relative CW complexes and is just redundant information

In addition, we could mention somewhere that the sequence of n-skeletons can be either finite or infinite. And the third condition is only needed if it's an infinite sequence. That's the idea.

I said this already, but the sequence is always infinite in some cases, it just stabilises. Making a distinction makes 0 sense.

Then the fact that a discrete space is a CW complex will indeed become a triviality. And the whole thing will also be slightly more accessible to people who have never seen the notion of CW complex.

It is already trivial. It is fine with the current phrasing, in fact it is useful for people who have not seen CW complexes since it gives an easy demonstration how it works.

If you both agree, I could do an edit as part of this PR. Or you can do one, and we'll go back and forth until we get a good formulation.

No

[prabau]

Or I could a separate PR with a suggested change to the definition.

[prabau]

@felixpernegger Why do you insist relating this to relative CW complexes? It's not directly relevant. And I am not suggesting to remove $X_{-1}=\emptyset$ at the start of the chain. That can remain.

[felixpernegger]

I am insisting on it, because relative CW complexes are a natural extension, and theorems (cellular approximation) generalise. So it is simply not natural to have a different def. for absolute CW complexes.
Your alternative makes the definition more complicated in my opinion. We dont even have to specify what $\partial D^n$ means techincally, it also follows definitionally.

[prabau]

Many sources use exactly what I am suggesting. Even the sources that you used and recommended.

[felixpernegger]

Then the fact that a discrete space is a CW complex will indeed become a triviality. And the whole thing will also be slightly more accessible to people who have never seen the notion of CW complex.

This is like saying: A path connected space is a connected spaces where any two points are joined by a path.

Then obviously path connected => Connected but the def wouldnt make sense

[felixpernegger]

what do you mean with the eyes?

[prabau]

there is a limited number of available emojis here. Not sure what the eyes mean. Just that the preceding comment did not make much sense to me.

Anyway, do you disagree that many sources use exactly what I am suggesting? Even the sources that you used and recommended.

[felixpernegger]

Some do yes (but not all), but that doesnt automatically mean thats ideal either. Also see https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/CWComplex/Classical/Basic.html#Topology.CWComplex (here an exact implementation is important)

But in general, we just had a PR with 180 comments sorted out. Can we maybe move on unless there are actual problems? (Which again is not the case here, the justification is 7 words)

[GeoffreySangston]

(1) Let's agree that eyes mean "I'm looking into this". This is, I think, a very serious point.

(2) I personally like @prabau's suggestion, because usually induction works by discussing the base case and then the inductive step, and this is analogous. I presently don't understand @felixpernegger's position though so please give me some time to consider it. It is my partner's birthday tonight though so I might not figure it out in time.

[prabau]

Let's sleep on it and reconsider this some other day.

[felixpernegger]

Can this PR be merged? Its entirely fine.

[GeoffreySangston]

@felixpernegger @prabau I think the whole thing comes down to what to treat as the base case for a CW complex, either the empty set or the $0$-skeleton. The relative cw complexes treat $A$ as the base case. I think whichever we go with should somehow clarify this. The way @prabau suggested seems strong to me if the $0$-skeleton is effectively the base case. However, if I think about building up a CW complex by adding in cells, then starting from empty space does seem pretty natural. I.e. I start from nothing, then I add the points, then I add the 1-cells, etc...

So now I'm actually leaning towards Felix's side here, which I think means the way of doing it in my previous comment #1766 (comment) might still be the way to go, though I think emphasizing the empty set as a base case for the attaching inductive process could also be good to do.

said this already, but the sequence is always infinite in some cases, it just stabilises. Making a distinction makes 0 sense.

Undoubtedly @prabau is well-aware of this, and that is what he means by finite. Shouldn't we engage with each other's points under a fair interpretation of them? Here the question is whether or not it's worth drawing attention to the fact that part (iii) is only needed in the non-finite dimensional (=not eventually stabilizes) case. I don't see why that makes 0 sense, since it potentially saves you from making redundant remarks everywhere you want to justify that a space is a finite cw complex. Since I think we might add Finite Dimensional CW Complex, a compromise is to not make this remark here and add it to the property file for Finite Dimensional CW Complex. On the other hand, it is rather trivial in the finite case, so we can let the reader see this as well.

[felixpernegger]

I havr two objections two finite chains:

1. Any implementation would not include this for practical reasons. See the mathlib ref I gave.

2. When is (would) a chain finite? Exactly when the J remains empty for almost all n. But of vourse im general we cant just require that J is nonempty, since there are CW complexes going up in i.e. every other step.
   So we would have to require the quite awkward:
   "Either the sequence is finite or J is nonempty for infinitely many n" to not have duplications.

From my perspective, its clear that a) J is finite and b) that X_n can stabilise. If not explicitly stated otherwise, a set csn always be empty.

[GeoffreySangston]

@felixpernegger I agree, but I just didn't think that's what @prabau was suggesting. Isn't it clear that a finite sequence in this context is the same thing as an eventually constant sequence?

[felixpernegger]

Not to me, no

[GeoffreySangston]

@felixpernegger I think the non-trivial content of @prabau's remark is that in the finite dimensional case the following is redundant:

a subspace $U \subseteq X$ is open iff $U \cap X_n$ open in $X_n$ for all $n \geq -1$.

[prabau]

I read all the discussion above, and I don't disagree with what has been said by either of you.

My concern was more practical. For a simple space, I want to be able to say something like: $X$ has a CW decomposition obtained by taking these 3 0-cells, this 1-cell, and these two 4-cells. And be done with it, without having to frame everything in a more abstract way involving filtrations, and stating that for all $n>4$ we have a filtration with $X_n=X$. Of course it's not wrong to say the last part, but why even bother if a simpler explanation is all we need.

For the particular case of a discrete space, I think everyone agrees that they are trivially a CW complex. Let me make a separate suggestion below, to make that even simpler (that will beat even the 6 word record that was claimed by Felix :-) :-) )

[prabau]

(Side remark: I still don't understand why make a big deal about relative CW complexes. "Relative CW complex" is not a property in pi-base, and as a topological property, it's meaningless since one can always choose $X_{-1}=X$. So I really don't understand what the concern was.

And also, in my previous suggestion about the rewrite of the definition of CW complex (which we don't have to do), I was not suggesting to remove the $X_{-1}=\emptyset$ part. So even if we explicitly say that $X_0$ is a discrete space, $X$ will still look like a relative CW complex. (And furthermore, I was still suggesting to add a sentence after the bullet points making note that a discrete space is obtained by "attaching 0-cells to the empty space", so nothing is lost.)
So really I don't understand what the issue was and would like to know.

@felixpernegger can you expand on what you were thinking?

[felixpernegger]

Relative CW complexes are relevant, even though we dont (and as you said shouldnt have them in pibase).
I do think pibase as a general reference should be conpatible with structure beyond it.

For example, one can phrase weakly contractible (or simply connected) entirely without naming groups (since those dont use group structures), but it is still a good practice

[prabau]

Well, ok. I don't dispute anything about that. And my proposal was also completely compatible with the notion of relative CW complex, since it still started with $X_{-1}=\emptyset$, and still mentioned that $X_0$ is obtained from $X_{-1}$ by attaching 0-cells (only in a separate sentence). So it's really the same thing.

[GeoffreySangston]

I'm guessing the answer is no, but is there any particular $A$ where CW complexes relative to A become an interesting/well studied and distinct topological property from (absolute) CW complexes?

[felixpernegger]

I dont know any and i would be surprised yeah

[prabau]

@felixpernegger Any comment on #1766 (comment)? If you apply it, I will approve.

[prabau]

@felixpernegger @GeoffreySangston You have not commented on #1766 (comment), which was my main point.

[felixpernegger]

@felixpernegger Any comment on #1766 (comment)? If you apply it, I will approve.

Didnt see the suggestions sorry. I think both versions are fine, I just apply it so we can move on.

[prabau]

Thanks. And please can you comment on #1766 (comment) (not the part about discrete spaces, the part before that).

[felixpernegger]

I read all the discussion above, and I don't disagree with what has been said by either of you.

My concern was more practical. For a simple space, I want to be able to say something like: X has a CW decomposition obtained by taking these 3 0-cells, this 1-cell, and these two 4-cells. And be done with it, without having to frame everything in a more abstract way involving filtrations, and stating that for all n > 4 we have a filtration with X n = X . Of course it's not wrong to say the last part, but why even bother if a simpler explanation is all we need.

For the particular case of a discrete space, I think everyone agrees that they are trivially a CW complex. Let me make a separate suggestion below, to make that even simpler (that will beat even the 6 word record that was claimed by Felix :-) :-) )

So, the way you stated it is pretty much how its done in textbooks. I.e. for sphere one says indeed, "1 zero cells, no cells up to n-1, then 1 n-cell" (+- indexing). I admittedly havent thought about this angle too much, but I think its safe to say that in these cases its simply implied for the reader that we take no further cells and weak topology trivially holds.

More generally, it seems to me one practically has to be a bit inprecise to prove some cell decomposition indeed is a CW complex for a partcular space. I.e. if for spheres one takes a different decomposition (the one with equator), its already a nontrivial task to formally show the defined CW complex (by the cells) is really homeomorphic to S^n

[felixpernegger]

This may have been suggested, but since were gonna be adding finite dim. CW complex anyways, why not make a comment in that file something along like: Note: The weak topology conditions can is fulfilled automatically
All the CW complexes we have right now (that I am aware of) will be finite dimensional, so we will really use that property for the trait and not the original CW complex one

[prabau]

Approving and leaving it to @GeoffreySangston to take one last look and do the merging.

[felixpernegger]

This may have been suggested, but since were gonna be adding finite dim. CW complex anyways, why not make a comment in that file something along like: Note: The weak topology conditions can is fulfilled automatically All the CW complexes we have right now (that I am aware of) will be finite dimensional, so we will really use that property for the trait and not the original CW complex one

@prabau would you be okay with this?

[GeoffreySangston]

@felixpernegger @GeoffreySangston You have not commented on #1766 (comment), which was my main point.

Oh sorry about that. The point you're making there is basically why I thought we should emphasize the second definition in the CW complex file, which is focused on the actual partition into cells, and probably much more natural to think about in smaller cases.

[prabau]

@GeoffreySangston I agree. I think we can later have another PR (or as part of the PR for finite dimensional CW complexes) which expands the second definition.

For now, if you are satisfied with the change for this PR, can you merge it?