Add CW complex trait to eight spaces (#1798) by Robby955 · Pull Request #1805 · pi-base/data

Robby955 · 2026-06-20T03:22:22Z

Adds the CW complex trait to the eight spaces listed in #1798 — S25, S139, S158, S168, S176, S198, S210, S225 — each with an explicit cell structure following the existing S169/S170 format (Hatcher, Ch. 0). S179 is left untouched (consistent-with-ZFC open case), and the secondary closed-world "everything else is not a CW complex" claim is not asserted, since it depends on the still-open #1769.

Open to all feedback and review.

Following the policy I also include this:
I used the AI program Claude Code CLI from Anthropic (model version Opus 4.8) to assist in these examples and the coding.

prabau · 2026-06-20T05:01:19Z

I am sure @felixpernegger will have more relevant comments about this.

No need to say "See the definition of CW complexes in Hatcher" everywhere. The definition, including a link to Hatcher, is available already in pi-base, and is just one click away. So that does not add anything.
On the other hand, references showing that a specific space is a CW complex would be useful if available.

prabau · 2026-06-20T05:08:13Z

+refs:
+ - zb: "1044.55001"
+ name: Algebraic Topology (Hatcher)
+---
+
+The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
+
+Equivalently, CW complexes are preserved by arbitrary disjoint unions.
+
+See the definition of CW complexes in {{zb:1044.55001}}.


Suggested change
refs:
- zb: "1044.55001"
name: Algebraic Topology (Hatcher)
---
The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
Equivalently, CW complexes are preserved by arbitrary disjoint unions.
See the definition of CW complexes in {{zb:1044.55001}}.
---
{S25|P240} and {S162|P240}, hence so is their disjoint union.
this is how we usually handle these kind of things, implicitly relying on the relevant meta-property.

prabau · 2026-06-20T05:18:51Z

@felixpernegger Several of the justifications here (for S176, 210, 225, etc) rely on some cell structure being locally finite and conclude from that. I assume "locally finite" has it usual meaning of a locally finite collection of sets in a topological space (each point contains a nbhd meeting only finitely many sets in the collection).

However, the definition of P240 (CW complex) in pi-base never mentioned locally finite anywhere. I don't even think it comes from the reformulation in the second characterization based on Hatcher A.2.

So what theorem somewhere could be quoted to justify this (simpler) approach? Since it's a relatively common case, would it be worth mentioning it somewhere in the definition page?

…nion meta-property

prabau · 2026-06-20T05:24:20Z

S162: not needed as it's already known to pi-base (from the discrete property):
https://topology.pi-base.org/spaces/S000162/properties/P000240

prabau · 2026-06-20T05:28:46Z

+
+The quotient $\mathbb R/\mathbb Z$ can be given a CW complex structure with one $0$-cell, namely the image of $\mathbb Z$, and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$, with both endpoints attached to the $0$-cell.
+
+This is the standard CW structure on a countable wedge of circles. The weak topology is the quotient topology described in the README, not the coarser topology on {S201}.


No need to mention the README (that's an internal thing that is not visible to users of pi-base). And no need to mention the coarser topology of S201. Just say something about the quotient topology defining X or something of that nature.

FYI: if you think the particular comment here has been resolved by a further commit, you can click on "Resolve conversation")

prabau · 2026-06-20T05:29:29Z

+value: true
+---
+
+The real line can be given a CW complex structure with $0$-cells indexed by $\mathbb Z$ and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$.


the 0-cells are the points of Z, not just indexed by Z.

All three addressed in the latest push: S162 file removed (it derives from the discrete-space theorem), S139 now describes the quotient topology directly (dropped the README/S201 mentions), and S025 says the 0-cells are the points of ℤ. Let me know if there is anything else I can do,Thanks.

(I think you meant to write this as a general comment, not specific to this file, as it will be hidden there)

…nce, give explicit/meta-property justifications

prabau · 2026-06-20T05:48:51Z

@Robby955 I really liked your previous explanations for all of this. But why did you remove the mention of "locally finite" cell structure? The newer version is more verbose and not clearer, on the contrary. If we can rely on some result involving locally finite cell structure, that would be optimal. That why I was asking @felixpernegger above.

If you are curious (and a little masochistic :) ), you can see a looong discussion in #1758 about the best way to present the notion of CW complex. We finally ended up with something in the first definition, with the thought that maybe things would be expanded further for the second equivalent definition. And maybe an extra piece about locally finite cell structures (CW structures?) would simplify things quite a bit when it applies (automatic "weak topology", etc)

@GeoffreySangston fyi

prabau · 2026-06-20T06:03:00Z

@Robby955 Thanks for all your changes. But instead of piling commits on top of commits, do you mind discussing things first? We would benefit from your insights as you seem quite knowledgeable about this area.

prabau · 2026-06-20T06:05:47Z

leaving it to @felixpernegger to discuss tomorrow. Main issue: "locally finite" and how best to use it/ present it in the definition file maybe.

Also, hope you can look in full detail at the changes, as I didn't do it myself.

Robby955 · 2026-06-20T06:10:50Z

Thanks, I'll discuss before pushing further. For a locally finite cell structure the weak-topology axiom is automatic, because local finiteness
makes "closed" a local condition, near each point only finitely many cells meet a neighborhood, so closedness is checkable cell-by-cell, and the weak topology then coincides with the given one. That's exactly why S25/S176/S210/S225 go through directly, and why S139 (countable wedge — not locally finite, infinitely many 1-cells at the basepoint) genuinely needs the quotient-topology argument instead. A single P240-page lemma "a locally finite cell structure is a CW complex" would let this whole class cite one result, which looks like where #1758 was heading.

prabau · 2026-06-20T06:19:55Z

Yeah, that's exactly what I'd like to see. So let's see tomorrow how to formulate this in the P240 page. There should be a theorem in the literature stating exactly this and we can just state this and quote the reference.

Side note: personally (and I am not the only one) I don't like the "weak topology" terminology too much. That's kind of older terminology, but in more modern terms it's the "final topology" wrt various maps (characteristic maps or embedding of each k-skeleton into X ?), i.e., the strongest topology (= finest topology) making these maps continuous. Quotient map is also "final topology". Just the opposite of the "weakest topology" (= coarsest topology). But I know it's common parlance in this context.

(I mistakenly wrote "initial topology" earlier when I meant "final topology".)

Robby955 · 2026-06-20T19:02:43Z

closing, see related AI policy discussions, thanks

Robby955 · 2026-06-20T03:22:22Z

Adds the CW complex trait to the eight spaces listed in #1798 — S25, S139, S158, S168, S176, S198, S210, S225 — each with an explicit cell structure following the existing S169/S170 format (Hatcher, Ch. 0). S179 is left untouched (consistent-with-ZFC open case), and the secondary closed-world "everything else is not a CW complex" claim is not asserted, since it depends on the still-open #1769.

Open to all feedback and review.

Following the policy I also include this:
I used the AI program Claude Code CLI from Anthropic (model version Opus 4.8) to assist in these examples and the coding.

prabau · 2026-06-20T05:01:19Z

I am sure @felixpernegger will have more relevant comments about this.

No need to say "See the definition of CW complexes in Hatcher" everywhere. The definition, including a link to Hatcher, is available already in pi-base, and is just one click away. So that does not add anything.
On the other hand, references showing that a specific space is a CW complex would be useful if available.

prabau · 2026-06-20T05:08:13Z

+refs:
+ - zb: "1044.55001"
+ name: Algebraic Topology (Hatcher)
+---
+
+The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
+
+Equivalently, CW complexes are preserved by arbitrary disjoint unions.
+
+See the definition of CW complexes in {{zb:1044.55001}}.


Suggested change
refs:
- zb: "1044.55001"
name: Algebraic Topology (Hatcher)
---
The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
Equivalently, CW complexes are preserved by arbitrary disjoint unions.
See the definition of CW complexes in {{zb:1044.55001}}.
---
{S25|P240} and {S162|P240}, hence so is their disjoint union.
this is how we usually handle these kind of things, implicitly relying on the relevant meta-property.

prabau · 2026-06-20T05:18:51Z

@felixpernegger Several of the justifications here (for S176, 210, 225, etc) rely on some cell structure being locally finite and conclude from that. I assume "locally finite" has it usual meaning of a locally finite collection of sets in a topological space (each point contains a nbhd meeting only finitely many sets in the collection).

However, the definition of P240 (CW complex) in pi-base never mentioned locally finite anywhere. I don't even think it comes from the reformulation in the second characterization based on Hatcher A.2.

So what theorem somewhere could be quoted to justify this (simpler) approach? Since it's a relatively common case, would it be worth mentioning it somewhere in the definition page?

…nion meta-property

prabau · 2026-06-20T05:24:20Z

S162: not needed as it's already known to pi-base (from the discrete property):
https://topology.pi-base.org/spaces/S000162/properties/P000240

prabau · 2026-06-20T05:28:46Z

+
+The quotient $\mathbb R/\mathbb Z$ can be given a CW complex structure with one $0$-cell, namely the image of $\mathbb Z$, and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$, with both endpoints attached to the $0$-cell.
+
+This is the standard CW structure on a countable wedge of circles. The weak topology is the quotient topology described in the README, not the coarser topology on {S201}.


No need to mention the README (that's an internal thing that is not visible to users of pi-base). And no need to mention the coarser topology of S201. Just say something about the quotient topology defining X or something of that nature.

FYI: if you think the particular comment here has been resolved by a further commit, you can click on "Resolve conversation")

prabau · 2026-06-20T05:29:29Z

+value: true
+---
+
+The real line can be given a CW complex structure with $0$-cells indexed by $\mathbb Z$ and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$.


the 0-cells are the points of Z, not just indexed by Z.

All three addressed in the latest push: S162 file removed (it derives from the discrete-space theorem), S139 now describes the quotient topology directly (dropped the README/S201 mentions), and S025 says the 0-cells are the points of ℤ. Let me know if there is anything else I can do,Thanks.

(I think you meant to write this as a general comment, not specific to this file, as it will be hidden there)

…nce, give explicit/meta-property justifications

prabau · 2026-06-20T05:48:51Z

@Robby955 I really liked your previous explanations for all of this. But why did you remove the mention of "locally finite" cell structure? The newer version is more verbose and not clearer, on the contrary. If we can rely on some result involving locally finite cell structure, that would be optimal. That why I was asking @felixpernegger above.

If you are curious (and a little masochistic :) ), you can see a looong discussion in #1758 about the best way to present the notion of CW complex. We finally ended up with something in the first definition, with the thought that maybe things would be expanded further for the second equivalent definition. And maybe an extra piece about locally finite cell structures (CW structures?) would simplify things quite a bit when it applies (automatic "weak topology", etc)

@GeoffreySangston fyi

prabau · 2026-06-20T06:03:00Z

@Robby955 Thanks for all your changes. But instead of piling commits on top of commits, do you mind discussing things first? We would benefit from your insights as you seem quite knowledgeable about this area.

prabau · 2026-06-20T06:05:47Z

leaving it to @felixpernegger to discuss tomorrow. Main issue: "locally finite" and how best to use it/ present it in the definition file maybe.

Also, hope you can look in full detail at the changes, as I didn't do it myself.

Robby955 · 2026-06-20T06:10:50Z

Thanks, I'll discuss before pushing further. For a locally finite cell structure the weak-topology axiom is automatic, because local finiteness
makes "closed" a local condition, near each point only finitely many cells meet a neighborhood, so closedness is checkable cell-by-cell, and the weak topology then coincides with the given one. That's exactly why S25/S176/S210/S225 go through directly, and why S139 (countable wedge — not locally finite, infinitely many 1-cells at the basepoint) genuinely needs the quotient-topology argument instead. A single P240-page lemma "a locally finite cell structure is a CW complex" would let this whole class cite one result, which looks like where #1758 was heading.

prabau · 2026-06-20T06:19:55Z

Yeah, that's exactly what I'd like to see. So let's see tomorrow how to formulate this in the P240 page. There should be a theorem in the literature stating exactly this and we can just state this and quote the reference.

Side note: personally (and I am not the only one) I don't like the "weak topology" terminology too much. That's kind of older terminology, but in more modern terms it's the "final topology" wrt various maps (characteristic maps or embedding of each k-skeleton into X ?), i.e., the strongest topology (= finest topology) making these maps continuous. Quotient map is also "final topology". Just the opposite of the "weakest topology" (= coarsest topology). But I know it's common parlance in this context.

(I mistakenly wrote "initial topology" earlier when I meant "final topology".)

Robby955 · 2026-06-20T19:02:43Z

closing, see related AI policy discussions, thanks

Robby955 · 2026-06-20T03:22:22Z

Adds the CW complex trait to the eight spaces listed in #1798 — S25, S139, S158, S168, S176, S198, S210, S225 — each with an explicit cell structure following the existing S169/S170 format (Hatcher, Ch. 0). S179 is left untouched (consistent-with-ZFC open case), and the secondary closed-world "everything else is not a CW complex" claim is not asserted, since it depends on the still-open #1769.

Open to all feedback and review.

Following the policy I also include this:
I used the AI program Claude Code CLI from Anthropic (model version Opus 4.8) to assist in these examples and the coding.

prabau · 2026-06-20T05:01:19Z

I am sure @felixpernegger will have more relevant comments about this.

No need to say "See the definition of CW complexes in Hatcher" everywhere. The definition, including a link to Hatcher, is available already in pi-base, and is just one click away. So that does not add anything.
On the other hand, references showing that a specific space is a CW complex would be useful if available.

prabau · 2026-06-20T05:08:13Z

+refs:
+ - zb: "1044.55001"
+ name: Algebraic Topology (Hatcher)
+---
+
+The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
+
+Equivalently, CW complexes are preserved by arbitrary disjoint unions.
+
+See the definition of CW complexes in {{zb:1044.55001}}.


Suggested change
refs:
- zb: "1044.55001"
name: Algebraic Topology (Hatcher)
---
The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
Equivalently, CW complexes are preserved by arbitrary disjoint unions.
See the definition of CW complexes in {{zb:1044.55001}}.
---
{S25|P240} and {S162|P240}, hence so is their disjoint union.
this is how we usually handle these kind of things, implicitly relying on the relevant meta-property.

prabau · 2026-06-20T05:18:51Z

@felixpernegger Several of the justifications here (for S176, 210, 225, etc) rely on some cell structure being locally finite and conclude from that. I assume "locally finite" has it usual meaning of a locally finite collection of sets in a topological space (each point contains a nbhd meeting only finitely many sets in the collection).

However, the definition of P240 (CW complex) in pi-base never mentioned locally finite anywhere. I don't even think it comes from the reformulation in the second characterization based on Hatcher A.2.

So what theorem somewhere could be quoted to justify this (simpler) approach? Since it's a relatively common case, would it be worth mentioning it somewhere in the definition page?

…nion meta-property

prabau · 2026-06-20T05:24:20Z

S162: not needed as it's already known to pi-base (from the discrete property):
https://topology.pi-base.org/spaces/S000162/properties/P000240

prabau · 2026-06-20T05:28:46Z

+
+The quotient $\mathbb R/\mathbb Z$ can be given a CW complex structure with one $0$-cell, namely the image of $\mathbb Z$, and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$, with both endpoints attached to the $0$-cell.
+
+This is the standard CW structure on a countable wedge of circles. The weak topology is the quotient topology described in the README, not the coarser topology on {S201}.


No need to mention the README (that's an internal thing that is not visible to users of pi-base). And no need to mention the coarser topology of S201. Just say something about the quotient topology defining X or something of that nature.

FYI: if you think the particular comment here has been resolved by a further commit, you can click on "Resolve conversation")

prabau · 2026-06-20T05:29:29Z

+value: true
+---
+
+The real line can be given a CW complex structure with $0$-cells indexed by $\mathbb Z$ and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$.


the 0-cells are the points of Z, not just indexed by Z.

All three addressed in the latest push: S162 file removed (it derives from the discrete-space theorem), S139 now describes the quotient topology directly (dropped the README/S201 mentions), and S025 says the 0-cells are the points of ℤ. Let me know if there is anything else I can do,Thanks.

(I think you meant to write this as a general comment, not specific to this file, as it will be hidden there)

…nce, give explicit/meta-property justifications

prabau · 2026-06-20T05:48:51Z

@Robby955 I really liked your previous explanations for all of this. But why did you remove the mention of "locally finite" cell structure? The newer version is more verbose and not clearer, on the contrary. If we can rely on some result involving locally finite cell structure, that would be optimal. That why I was asking @felixpernegger above.

If you are curious (and a little masochistic :) ), you can see a looong discussion in #1758 about the best way to present the notion of CW complex. We finally ended up with something in the first definition, with the thought that maybe things would be expanded further for the second equivalent definition. And maybe an extra piece about locally finite cell structures (CW structures?) would simplify things quite a bit when it applies (automatic "weak topology", etc)

@GeoffreySangston fyi

prabau · 2026-06-20T06:03:00Z

@Robby955 Thanks for all your changes. But instead of piling commits on top of commits, do you mind discussing things first? We would benefit from your insights as you seem quite knowledgeable about this area.

prabau · 2026-06-20T06:05:47Z

leaving it to @felixpernegger to discuss tomorrow. Main issue: "locally finite" and how best to use it/ present it in the definition file maybe.

Also, hope you can look in full detail at the changes, as I didn't do it myself.

Robby955 · 2026-06-20T06:10:50Z

Thanks, I'll discuss before pushing further. For a locally finite cell structure the weak-topology axiom is automatic, because local finiteness
makes "closed" a local condition, near each point only finitely many cells meet a neighborhood, so closedness is checkable cell-by-cell, and the weak topology then coincides with the given one. That's exactly why S25/S176/S210/S225 go through directly, and why S139 (countable wedge — not locally finite, infinitely many 1-cells at the basepoint) genuinely needs the quotient-topology argument instead. A single P240-page lemma "a locally finite cell structure is a CW complex" would let this whole class cite one result, which looks like where #1758 was heading.

prabau · 2026-06-20T06:19:55Z

Yeah, that's exactly what I'd like to see. So let's see tomorrow how to formulate this in the P240 page. There should be a theorem in the literature stating exactly this and we can just state this and quote the reference.

Side note: personally (and I am not the only one) I don't like the "weak topology" terminology too much. That's kind of older terminology, but in more modern terms it's the "final topology" wrt various maps (characteristic maps or embedding of each k-skeleton into X ?), i.e., the strongest topology (= finest topology) making these maps continuous. Quotient map is also "final topology". Just the opposite of the "weakest topology" (= coarsest topology). But I know it's common parlance in this context.

(I mistakenly wrote "initial topology" earlier when I meant "final topology".)

Robby955 · 2026-06-20T19:02:43Z

closing, see related AI policy discussions, thanks

Robby955 · 2026-06-20T03:22:22Z

Adds the CW complex trait to the eight spaces listed in #1798 — S25, S139, S158, S168, S176, S198, S210, S225 — each with an explicit cell structure following the existing S169/S170 format (Hatcher, Ch. 0). S179 is left untouched (consistent-with-ZFC open case), and the secondary closed-world "everything else is not a CW complex" claim is not asserted, since it depends on the still-open #1769.

Open to all feedback and review.

Following the policy I also include this:
I used the AI program Claude Code CLI from Anthropic (model version Opus 4.8) to assist in these examples and the coding.

prabau · 2026-06-20T05:01:19Z

I am sure @felixpernegger will have more relevant comments about this.

No need to say "See the definition of CW complexes in Hatcher" everywhere. The definition, including a link to Hatcher, is available already in pi-base, and is just one click away. So that does not add anything.
On the other hand, references showing that a specific space is a CW complex would be useful if available.

prabau · 2026-06-20T05:08:13Z

+refs:
+ - zb: "1044.55001"
+ name: Algebraic Topology (Hatcher)
+---
+
+The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
+
+Equivalently, CW complexes are preserved by arbitrary disjoint unions.
+
+See the definition of CW complexes in {{zb:1044.55001}}.


Suggested change
refs:
- zb: "1044.55001"
name: Algebraic Topology (Hatcher)
---
The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
Equivalently, CW complexes are preserved by arbitrary disjoint unions.
See the definition of CW complexes in {{zb:1044.55001}}.
---
{S25|P240} and {S162|P240}, hence so is their disjoint union.
this is how we usually handle these kind of things, implicitly relying on the relevant meta-property.

prabau · 2026-06-20T05:18:51Z

@felixpernegger Several of the justifications here (for S176, 210, 225, etc) rely on some cell structure being locally finite and conclude from that. I assume "locally finite" has it usual meaning of a locally finite collection of sets in a topological space (each point contains a nbhd meeting only finitely many sets in the collection).

However, the definition of P240 (CW complex) in pi-base never mentioned locally finite anywhere. I don't even think it comes from the reformulation in the second characterization based on Hatcher A.2.

So what theorem somewhere could be quoted to justify this (simpler) approach? Since it's a relatively common case, would it be worth mentioning it somewhere in the definition page?

…nion meta-property

prabau · 2026-06-20T05:24:20Z

S162: not needed as it's already known to pi-base (from the discrete property):
https://topology.pi-base.org/spaces/S000162/properties/P000240

prabau · 2026-06-20T05:28:46Z

+
+The quotient $\mathbb R/\mathbb Z$ can be given a CW complex structure with one $0$-cell, namely the image of $\mathbb Z$, and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$, with both endpoints attached to the $0$-cell.
+
+This is the standard CW structure on a countable wedge of circles. The weak topology is the quotient topology described in the README, not the coarser topology on {S201}.


No need to mention the README (that's an internal thing that is not visible to users of pi-base). And no need to mention the coarser topology of S201. Just say something about the quotient topology defining X or something of that nature.

FYI: if you think the particular comment here has been resolved by a further commit, you can click on "Resolve conversation")

prabau · 2026-06-20T05:29:29Z

+value: true
+---
+
+The real line can be given a CW complex structure with $0$-cells indexed by $\mathbb Z$ and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$.


the 0-cells are the points of Z, not just indexed by Z.

All three addressed in the latest push: S162 file removed (it derives from the discrete-space theorem), S139 now describes the quotient topology directly (dropped the README/S201 mentions), and S025 says the 0-cells are the points of ℤ. Let me know if there is anything else I can do,Thanks.

(I think you meant to write this as a general comment, not specific to this file, as it will be hidden there)

…nce, give explicit/meta-property justifications

prabau · 2026-06-20T05:48:51Z

@Robby955 I really liked your previous explanations for all of this. But why did you remove the mention of "locally finite" cell structure? The newer version is more verbose and not clearer, on the contrary. If we can rely on some result involving locally finite cell structure, that would be optimal. That why I was asking @felixpernegger above.

If you are curious (and a little masochistic :) ), you can see a looong discussion in #1758 about the best way to present the notion of CW complex. We finally ended up with something in the first definition, with the thought that maybe things would be expanded further for the second equivalent definition. And maybe an extra piece about locally finite cell structures (CW structures?) would simplify things quite a bit when it applies (automatic "weak topology", etc)

@GeoffreySangston fyi

prabau · 2026-06-20T06:03:00Z

@Robby955 Thanks for all your changes. But instead of piling commits on top of commits, do you mind discussing things first? We would benefit from your insights as you seem quite knowledgeable about this area.

prabau · 2026-06-20T06:05:47Z

leaving it to @felixpernegger to discuss tomorrow. Main issue: "locally finite" and how best to use it/ present it in the definition file maybe.

Also, hope you can look in full detail at the changes, as I didn't do it myself.

Robby955 · 2026-06-20T06:10:50Z

Thanks, I'll discuss before pushing further. For a locally finite cell structure the weak-topology axiom is automatic, because local finiteness
makes "closed" a local condition, near each point only finitely many cells meet a neighborhood, so closedness is checkable cell-by-cell, and the weak topology then coincides with the given one. That's exactly why S25/S176/S210/S225 go through directly, and why S139 (countable wedge — not locally finite, infinitely many 1-cells at the basepoint) genuinely needs the quotient-topology argument instead. A single P240-page lemma "a locally finite cell structure is a CW complex" would let this whole class cite one result, which looks like where #1758 was heading.

prabau · 2026-06-20T06:19:55Z

Yeah, that's exactly what I'd like to see. So let's see tomorrow how to formulate this in the P240 page. There should be a theorem in the literature stating exactly this and we can just state this and quote the reference.

Side note: personally (and I am not the only one) I don't like the "weak topology" terminology too much. That's kind of older terminology, but in more modern terms it's the "final topology" wrt various maps (characteristic maps or embedding of each k-skeleton into X ?), i.e., the strongest topology (= finest topology) making these maps continuous. Quotient map is also "final topology". Just the opposite of the "weakest topology" (= coarsest topology). But I know it's common parlance in this context.

(I mistakenly wrote "initial topology" earlier when I meant "final topology".)

Robby955 · 2026-06-20T19:02:43Z

closing, see related AI policy discussions, thanks

Robby955 · 2026-06-20T03:22:22Z

Adds the CW complex trait to the eight spaces listed in #1798 — S25, S139, S158, S168, S176, S198, S210, S225 — each with an explicit cell structure following the existing S169/S170 format (Hatcher, Ch. 0). S179 is left untouched (consistent-with-ZFC open case), and the secondary closed-world "everything else is not a CW complex" claim is not asserted, since it depends on the still-open #1769.

Open to all feedback and review.

Following the policy I also include this:
I used the AI program Claude Code CLI from Anthropic (model version Opus 4.8) to assist in these examples and the coding.

prabau · 2026-06-20T05:01:19Z

I am sure @felixpernegger will have more relevant comments about this.

No need to say "See the definition of CW complexes in Hatcher" everywhere. The definition, including a link to Hatcher, is available already in pi-base, and is just one click away. So that does not add anything.
On the other hand, references showing that a specific space is a CW complex would be useful if available.

prabau · 2026-06-20T05:08:13Z

+refs:
+ - zb: "1044.55001"
+ name: Algebraic Topology (Hatcher)
+---
+
+The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
+
+Equivalently, CW complexes are preserved by arbitrary disjoint unions.
+
+See the definition of CW complexes in {{zb:1044.55001}}.


Suggested change
refs:
- zb: "1044.55001"
name: Algebraic Topology (Hatcher)
---
The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
Equivalently, CW complexes are preserved by arbitrary disjoint unions.
See the definition of CW complexes in {{zb:1044.55001}}.
---
{S25|P240} and {S162|P240}, hence so is their disjoint union.
this is how we usually handle these kind of things, implicitly relying on the relevant meta-property.

prabau · 2026-06-20T05:18:51Z

@felixpernegger Several of the justifications here (for S176, 210, 225, etc) rely on some cell structure being locally finite and conclude from that. I assume "locally finite" has it usual meaning of a locally finite collection of sets in a topological space (each point contains a nbhd meeting only finitely many sets in the collection).

However, the definition of P240 (CW complex) in pi-base never mentioned locally finite anywhere. I don't even think it comes from the reformulation in the second characterization based on Hatcher A.2.

So what theorem somewhere could be quoted to justify this (simpler) approach? Since it's a relatively common case, would it be worth mentioning it somewhere in the definition page?

…nion meta-property

prabau · 2026-06-20T05:24:20Z

S162: not needed as it's already known to pi-base (from the discrete property):
https://topology.pi-base.org/spaces/S000162/properties/P000240

prabau · 2026-06-20T05:28:46Z

+
+The quotient $\mathbb R/\mathbb Z$ can be given a CW complex structure with one $0$-cell, namely the image of $\mathbb Z$, and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$, with both endpoints attached to the $0$-cell.
+
+This is the standard CW structure on a countable wedge of circles. The weak topology is the quotient topology described in the README, not the coarser topology on {S201}.


No need to mention the README (that's an internal thing that is not visible to users of pi-base). And no need to mention the coarser topology of S201. Just say something about the quotient topology defining X or something of that nature.

FYI: if you think the particular comment here has been resolved by a further commit, you can click on "Resolve conversation")

prabau · 2026-06-20T05:29:29Z

+value: true
+---
+
+The real line can be given a CW complex structure with $0$-cells indexed by $\mathbb Z$ and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$.


the 0-cells are the points of Z, not just indexed by Z.

All three addressed in the latest push: S162 file removed (it derives from the discrete-space theorem), S139 now describes the quotient topology directly (dropped the README/S201 mentions), and S025 says the 0-cells are the points of ℤ. Let me know if there is anything else I can do,Thanks.

(I think you meant to write this as a general comment, not specific to this file, as it will be hidden there)

…nce, give explicit/meta-property justifications

prabau · 2026-06-20T05:48:51Z

@Robby955 I really liked your previous explanations for all of this. But why did you remove the mention of "locally finite" cell structure? The newer version is more verbose and not clearer, on the contrary. If we can rely on some result involving locally finite cell structure, that would be optimal. That why I was asking @felixpernegger above.

If you are curious (and a little masochistic :) ), you can see a looong discussion in #1758 about the best way to present the notion of CW complex. We finally ended up with something in the first definition, with the thought that maybe things would be expanded further for the second equivalent definition. And maybe an extra piece about locally finite cell structures (CW structures?) would simplify things quite a bit when it applies (automatic "weak topology", etc)

@GeoffreySangston fyi

prabau · 2026-06-20T06:03:00Z

@Robby955 Thanks for all your changes. But instead of piling commits on top of commits, do you mind discussing things first? We would benefit from your insights as you seem quite knowledgeable about this area.

prabau · 2026-06-20T06:05:47Z

leaving it to @felixpernegger to discuss tomorrow. Main issue: "locally finite" and how best to use it/ present it in the definition file maybe.

Also, hope you can look in full detail at the changes, as I didn't do it myself.

Robby955 · 2026-06-20T06:10:50Z

Thanks, I'll discuss before pushing further. For a locally finite cell structure the weak-topology axiom is automatic, because local finiteness
makes "closed" a local condition, near each point only finitely many cells meet a neighborhood, so closedness is checkable cell-by-cell, and the weak topology then coincides with the given one. That's exactly why S25/S176/S210/S225 go through directly, and why S139 (countable wedge — not locally finite, infinitely many 1-cells at the basepoint) genuinely needs the quotient-topology argument instead. A single P240-page lemma "a locally finite cell structure is a CW complex" would let this whole class cite one result, which looks like where #1758 was heading.

prabau · 2026-06-20T06:19:55Z

Yeah, that's exactly what I'd like to see. So let's see tomorrow how to formulate this in the P240 page. There should be a theorem in the literature stating exactly this and we can just state this and quote the reference.

Side note: personally (and I am not the only one) I don't like the "weak topology" terminology too much. That's kind of older terminology, but in more modern terms it's the "final topology" wrt various maps (characteristic maps or embedding of each k-skeleton into X ?), i.e., the strongest topology (= finest topology) making these maps continuous. Quotient map is also "final topology". Just the opposite of the "weakest topology" (= coarsest topology). But I know it's common parlance in this context.

(I mistakenly wrote "initial topology" earlier when I meant "final topology".)

Robby955 · 2026-06-20T19:02:43Z

closing, see related AI policy discussions, thanks

Robby955 · 2026-06-20T03:22:22Z

Adds the CW complex trait to the eight spaces listed in #1798 — S25, S139, S158, S168, S176, S198, S210, S225 — each with an explicit cell structure following the existing S169/S170 format (Hatcher, Ch. 0). S179 is left untouched (consistent-with-ZFC open case), and the secondary closed-world "everything else is not a CW complex" claim is not asserted, since it depends on the still-open #1769.

Open to all feedback and review.

Following the policy I also include this:
I used the AI program Claude Code CLI from Anthropic (model version Opus 4.8) to assist in these examples and the coding.

prabau · 2026-06-20T05:01:19Z

I am sure @felixpernegger will have more relevant comments about this.

No need to say "See the definition of CW complexes in Hatcher" everywhere. The definition, including a link to Hatcher, is available already in pi-base, and is just one click away. So that does not add anything.
On the other hand, references showing that a specific space is a CW complex would be useful if available.

prabau · 2026-06-20T05:08:13Z

+refs:
+ - zb: "1044.55001"
+ name: Algebraic Topology (Hatcher)
+---
+
+The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
+
+Equivalently, CW complexes are preserved by arbitrary disjoint unions.
+
+See the definition of CW complexes in {{zb:1044.55001}}.


Suggested change
refs:
- zb: "1044.55001"
name: Algebraic Topology (Hatcher)
---
The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
Equivalently, CW complexes are preserved by arbitrary disjoint unions.
See the definition of CW complexes in {{zb:1044.55001}}.
---
{S25|P240} and {S162|P240}, hence so is their disjoint union.
this is how we usually handle these kind of things, implicitly relying on the relevant meta-property.

prabau · 2026-06-20T05:18:51Z

@felixpernegger Several of the justifications here (for S176, 210, 225, etc) rely on some cell structure being locally finite and conclude from that. I assume "locally finite" has it usual meaning of a locally finite collection of sets in a topological space (each point contains a nbhd meeting only finitely many sets in the collection).

However, the definition of P240 (CW complex) in pi-base never mentioned locally finite anywhere. I don't even think it comes from the reformulation in the second characterization based on Hatcher A.2.

So what theorem somewhere could be quoted to justify this (simpler) approach? Since it's a relatively common case, would it be worth mentioning it somewhere in the definition page?

…nion meta-property

prabau · 2026-06-20T05:24:20Z

S162: not needed as it's already known to pi-base (from the discrete property):
https://topology.pi-base.org/spaces/S000162/properties/P000240

prabau · 2026-06-20T05:28:46Z

+
+The quotient $\mathbb R/\mathbb Z$ can be given a CW complex structure with one $0$-cell, namely the image of $\mathbb Z$, and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$, with both endpoints attached to the $0$-cell.
+
+This is the standard CW structure on a countable wedge of circles. The weak topology is the quotient topology described in the README, not the coarser topology on {S201}.


No need to mention the README (that's an internal thing that is not visible to users of pi-base). And no need to mention the coarser topology of S201. Just say something about the quotient topology defining X or something of that nature.

FYI: if you think the particular comment here has been resolved by a further commit, you can click on "Resolve conversation")

prabau · 2026-06-20T05:29:29Z

+value: true
+---
+
+The real line can be given a CW complex structure with $0$-cells indexed by $\mathbb Z$ and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$.


the 0-cells are the points of Z, not just indexed by Z.

All three addressed in the latest push: S162 file removed (it derives from the discrete-space theorem), S139 now describes the quotient topology directly (dropped the README/S201 mentions), and S025 says the 0-cells are the points of ℤ. Let me know if there is anything else I can do,Thanks.

(I think you meant to write this as a general comment, not specific to this file, as it will be hidden there)

…nce, give explicit/meta-property justifications

prabau · 2026-06-20T05:48:51Z

@Robby955 I really liked your previous explanations for all of this. But why did you remove the mention of "locally finite" cell structure? The newer version is more verbose and not clearer, on the contrary. If we can rely on some result involving locally finite cell structure, that would be optimal. That why I was asking @felixpernegger above.

If you are curious (and a little masochistic :) ), you can see a looong discussion in #1758 about the best way to present the notion of CW complex. We finally ended up with something in the first definition, with the thought that maybe things would be expanded further for the second equivalent definition. And maybe an extra piece about locally finite cell structures (CW structures?) would simplify things quite a bit when it applies (automatic "weak topology", etc)

@GeoffreySangston fyi

prabau · 2026-06-20T06:03:00Z

@Robby955 Thanks for all your changes. But instead of piling commits on top of commits, do you mind discussing things first? We would benefit from your insights as you seem quite knowledgeable about this area.

prabau · 2026-06-20T06:05:47Z

leaving it to @felixpernegger to discuss tomorrow. Main issue: "locally finite" and how best to use it/ present it in the definition file maybe.

Also, hope you can look in full detail at the changes, as I didn't do it myself.

Robby955 · 2026-06-20T06:10:50Z

Thanks, I'll discuss before pushing further. For a locally finite cell structure the weak-topology axiom is automatic, because local finiteness
makes "closed" a local condition, near each point only finitely many cells meet a neighborhood, so closedness is checkable cell-by-cell, and the weak topology then coincides with the given one. That's exactly why S25/S176/S210/S225 go through directly, and why S139 (countable wedge — not locally finite, infinitely many 1-cells at the basepoint) genuinely needs the quotient-topology argument instead. A single P240-page lemma "a locally finite cell structure is a CW complex" would let this whole class cite one result, which looks like where #1758 was heading.

prabau · 2026-06-20T06:19:55Z

Yeah, that's exactly what I'd like to see. So let's see tomorrow how to formulate this in the P240 page. There should be a theorem in the literature stating exactly this and we can just state this and quote the reference.

Side note: personally (and I am not the only one) I don't like the "weak topology" terminology too much. That's kind of older terminology, but in more modern terms it's the "final topology" wrt various maps (characteristic maps or embedding of each k-skeleton into X ?), i.e., the strongest topology (= finest topology) making these maps continuous. Quotient map is also "final topology". Just the opposite of the "weakest topology" (= coarsest topology). But I know it's common parlance in this context.

(I mistakenly wrote "initial topology" earlier when I meant "final topology".)

Robby955 · 2026-06-20T19:02:43Z

closing, see related AI policy discussions, thanks

Robby955 · 2026-06-20T03:22:22Z

Adds the CW complex trait to the eight spaces listed in #1798 — S25, S139, S158, S168, S176, S198, S210, S225 — each with an explicit cell structure following the existing S169/S170 format (Hatcher, Ch. 0). S179 is left untouched (consistent-with-ZFC open case), and the secondary closed-world "everything else is not a CW complex" claim is not asserted, since it depends on the still-open #1769.

Open to all feedback and review.

Following the policy I also include this:
I used the AI program Claude Code CLI from Anthropic (model version Opus 4.8) to assist in these examples and the coding.

prabau · 2026-06-20T05:01:19Z

I am sure @felixpernegger will have more relevant comments about this.

No need to say "See the definition of CW complexes in Hatcher" everywhere. The definition, including a link to Hatcher, is available already in pi-base, and is just one click away. So that does not add anything.
On the other hand, references showing that a specific space is a CW complex would be useful if available.

prabau · 2026-06-20T05:08:13Z

+refs:
+ - zb: "1044.55001"
+ name: Algebraic Topology (Hatcher)
+---
+
+The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
+
+Equivalently, CW complexes are preserved by arbitrary disjoint unions.
+
+See the definition of CW complexes in {{zb:1044.55001}}.


Suggested change
refs:
- zb: "1044.55001"
name: Algebraic Topology (Hatcher)
---
The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
Equivalently, CW complexes are preserved by arbitrary disjoint unions.
See the definition of CW complexes in {{zb:1044.55001}}.
---
{S25|P240} and {S162|P240}, hence so is their disjoint union.
this is how we usually handle these kind of things, implicitly relying on the relevant meta-property.

prabau · 2026-06-20T05:18:51Z

@felixpernegger Several of the justifications here (for S176, 210, 225, etc) rely on some cell structure being locally finite and conclude from that. I assume "locally finite" has it usual meaning of a locally finite collection of sets in a topological space (each point contains a nbhd meeting only finitely many sets in the collection).

However, the definition of P240 (CW complex) in pi-base never mentioned locally finite anywhere. I don't even think it comes from the reformulation in the second characterization based on Hatcher A.2.

So what theorem somewhere could be quoted to justify this (simpler) approach? Since it's a relatively common case, would it be worth mentioning it somewhere in the definition page?

…nion meta-property

prabau · 2026-06-20T05:24:20Z

S162: not needed as it's already known to pi-base (from the discrete property):
https://topology.pi-base.org/spaces/S000162/properties/P000240

prabau · 2026-06-20T05:28:46Z

+
+The quotient $\mathbb R/\mathbb Z$ can be given a CW complex structure with one $0$-cell, namely the image of $\mathbb Z$, and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$, with both endpoints attached to the $0$-cell.
+
+This is the standard CW structure on a countable wedge of circles. The weak topology is the quotient topology described in the README, not the coarser topology on {S201}.


No need to mention the README (that's an internal thing that is not visible to users of pi-base). And no need to mention the coarser topology of S201. Just say something about the quotient topology defining X or something of that nature.

FYI: if you think the particular comment here has been resolved by a further commit, you can click on "Resolve conversation")

prabau · 2026-06-20T05:29:29Z

+value: true
+---
+
+The real line can be given a CW complex structure with $0$-cells indexed by $\mathbb Z$ and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$.


the 0-cells are the points of Z, not just indexed by Z.

All three addressed in the latest push: S162 file removed (it derives from the discrete-space theorem), S139 now describes the quotient topology directly (dropped the README/S201 mentions), and S025 says the 0-cells are the points of ℤ. Let me know if there is anything else I can do,Thanks.

(I think you meant to write this as a general comment, not specific to this file, as it will be hidden there)

…nce, give explicit/meta-property justifications

prabau · 2026-06-20T05:48:51Z

@Robby955 I really liked your previous explanations for all of this. But why did you remove the mention of "locally finite" cell structure? The newer version is more verbose and not clearer, on the contrary. If we can rely on some result involving locally finite cell structure, that would be optimal. That why I was asking @felixpernegger above.

If you are curious (and a little masochistic :) ), you can see a looong discussion in #1758 about the best way to present the notion of CW complex. We finally ended up with something in the first definition, with the thought that maybe things would be expanded further for the second equivalent definition. And maybe an extra piece about locally finite cell structures (CW structures?) would simplify things quite a bit when it applies (automatic "weak topology", etc)

@GeoffreySangston fyi

prabau · 2026-06-20T06:03:00Z

@Robby955 Thanks for all your changes. But instead of piling commits on top of commits, do you mind discussing things first? We would benefit from your insights as you seem quite knowledgeable about this area.

prabau · 2026-06-20T06:05:47Z

leaving it to @felixpernegger to discuss tomorrow. Main issue: "locally finite" and how best to use it/ present it in the definition file maybe.

Also, hope you can look in full detail at the changes, as I didn't do it myself.

Robby955 · 2026-06-20T06:10:50Z

Thanks, I'll discuss before pushing further. For a locally finite cell structure the weak-topology axiom is automatic, because local finiteness
makes "closed" a local condition, near each point only finitely many cells meet a neighborhood, so closedness is checkable cell-by-cell, and the weak topology then coincides with the given one. That's exactly why S25/S176/S210/S225 go through directly, and why S139 (countable wedge — not locally finite, infinitely many 1-cells at the basepoint) genuinely needs the quotient-topology argument instead. A single P240-page lemma "a locally finite cell structure is a CW complex" would let this whole class cite one result, which looks like where #1758 was heading.

prabau · 2026-06-20T06:19:55Z

Yeah, that's exactly what I'd like to see. So let's see tomorrow how to formulate this in the P240 page. There should be a theorem in the literature stating exactly this and we can just state this and quote the reference.

Side note: personally (and I am not the only one) I don't like the "weak topology" terminology too much. That's kind of older terminology, but in more modern terms it's the "final topology" wrt various maps (characteristic maps or embedding of each k-skeleton into X ?), i.e., the strongest topology (= finest topology) making these maps continuous. Quotient map is also "final topology". Just the opposite of the "weakest topology" (= coarsest topology). But I know it's common parlance in this context.

(I mistakenly wrote "initial topology" earlier when I meant "final topology".)

Robby955 · 2026-06-20T19:02:43Z

closing, see related AI policy discussions, thanks

Robby955 · 2026-06-20T03:22:22Z

Adds the CW complex trait to the eight spaces listed in #1798 — S25, S139, S158, S168, S176, S198, S210, S225 — each with an explicit cell structure following the existing S169/S170 format (Hatcher, Ch. 0). S179 is left untouched (consistent-with-ZFC open case), and the secondary closed-world "everything else is not a CW complex" claim is not asserted, since it depends on the still-open #1769.

Open to all feedback and review.

Following the policy I also include this:
I used the AI program Claude Code CLI from Anthropic (model version Opus 4.8) to assist in these examples and the coding.

prabau · 2026-06-20T05:01:19Z

I am sure @felixpernegger will have more relevant comments about this.

No need to say "See the definition of CW complexes in Hatcher" everywhere. The definition, including a link to Hatcher, is available already in pi-base, and is just one click away. So that does not add anything.
On the other hand, references showing that a specific space is a CW complex would be useful if available.

prabau · 2026-06-20T05:08:13Z

+refs:
+ - zb: "1044.55001"
+ name: Algebraic Topology (Hatcher)
+---
+
+The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
+
+Equivalently, CW complexes are preserved by arbitrary disjoint unions.
+
+See the definition of CW complexes in {{zb:1044.55001}}.


Suggested change
refs:
- zb: "1044.55001"
name: Algebraic Topology (Hatcher)
---
The space $\mathbb R\sqcup\{\star\}$ is the disjoint union of the real line and a singleton. Use the CW structure on $\mathbb R$ from {S25|P240}, and add $\{\star\}$ as one further $0$-cell in a separate component.
Equivalently, CW complexes are preserved by arbitrary disjoint unions.
See the definition of CW complexes in {{zb:1044.55001}}.
---
{S25|P240} and {S162|P240}, hence so is their disjoint union.
this is how we usually handle these kind of things, implicitly relying on the relevant meta-property.

prabau · 2026-06-20T05:18:51Z

@felixpernegger Several of the justifications here (for S176, 210, 225, etc) rely on some cell structure being locally finite and conclude from that. I assume "locally finite" has it usual meaning of a locally finite collection of sets in a topological space (each point contains a nbhd meeting only finitely many sets in the collection).

However, the definition of P240 (CW complex) in pi-base never mentioned locally finite anywhere. I don't even think it comes from the reformulation in the second characterization based on Hatcher A.2.

So what theorem somewhere could be quoted to justify this (simpler) approach? Since it's a relatively common case, would it be worth mentioning it somewhere in the definition page?

…nion meta-property

prabau · 2026-06-20T05:24:20Z

S162: not needed as it's already known to pi-base (from the discrete property):
https://topology.pi-base.org/spaces/S000162/properties/P000240

prabau · 2026-06-20T05:28:46Z

+
+The quotient $\mathbb R/\mathbb Z$ can be given a CW complex structure with one $0$-cell, namely the image of $\mathbb Z$, and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$, with both endpoints attached to the $0$-cell.
+
+This is the standard CW structure on a countable wedge of circles. The weak topology is the quotient topology described in the README, not the coarser topology on {S201}.


No need to mention the README (that's an internal thing that is not visible to users of pi-base). And no need to mention the coarser topology of S201. Just say something about the quotient topology defining X or something of that nature.

FYI: if you think the particular comment here has been resolved by a further commit, you can click on "Resolve conversation")

prabau · 2026-06-20T05:29:29Z

+value: true
+---
+
+The real line can be given a CW complex structure with $0$-cells indexed by $\mathbb Z$ and one $1$-cell for each interval $[n,n+1]$, where $n \in \mathbb Z$.


the 0-cells are the points of Z, not just indexed by Z.

All three addressed in the latest push: S162 file removed (it derives from the discrete-space theorem), S139 now describes the quotient topology directly (dropped the README/S201 mentions), and S025 says the 0-cells are the points of ℤ. Let me know if there is anything else I can do,Thanks.

(I think you meant to write this as a general comment, not specific to this file, as it will be hidden there)

…nce, give explicit/meta-property justifications

prabau · 2026-06-20T05:48:51Z

@Robby955 I really liked your previous explanations for all of this. But why did you remove the mention of "locally finite" cell structure? The newer version is more verbose and not clearer, on the contrary. If we can rely on some result involving locally finite cell structure, that would be optimal. That why I was asking @felixpernegger above.

If you are curious (and a little masochistic :) ), you can see a looong discussion in #1758 about the best way to present the notion of CW complex. We finally ended up with something in the first definition, with the thought that maybe things would be expanded further for the second equivalent definition. And maybe an extra piece about locally finite cell structures (CW structures?) would simplify things quite a bit when it applies (automatic "weak topology", etc)

@GeoffreySangston fyi

prabau · 2026-06-20T06:03:00Z

@Robby955 Thanks for all your changes. But instead of piling commits on top of commits, do you mind discussing things first? We would benefit from your insights as you seem quite knowledgeable about this area.

prabau · 2026-06-20T06:05:47Z

leaving it to @felixpernegger to discuss tomorrow. Main issue: "locally finite" and how best to use it/ present it in the definition file maybe.

Also, hope you can look in full detail at the changes, as I didn't do it myself.

Robby955 · 2026-06-20T06:10:50Z

Thanks, I'll discuss before pushing further. For a locally finite cell structure the weak-topology axiom is automatic, because local finiteness
makes "closed" a local condition, near each point only finitely many cells meet a neighborhood, so closedness is checkable cell-by-cell, and the weak topology then coincides with the given one. That's exactly why S25/S176/S210/S225 go through directly, and why S139 (countable wedge — not locally finite, infinitely many 1-cells at the basepoint) genuinely needs the quotient-topology argument instead. A single P240-page lemma "a locally finite cell structure is a CW complex" would let this whole class cite one result, which looks like where #1758 was heading.

prabau · 2026-06-20T06:19:55Z

Yeah, that's exactly what I'd like to see. So let's see tomorrow how to formulate this in the P240 page. There should be a theorem in the literature stating exactly this and we can just state this and quote the reference.

Side note: personally (and I am not the only one) I don't like the "weak topology" terminology too much. That's kind of older terminology, but in more modern terms it's the "final topology" wrt various maps (characteristic maps or embedding of each k-skeleton into X ?), i.e., the strongest topology (= finest topology) making these maps continuous. Quotient map is also "final topology". Just the opposite of the "weakest topology" (= coarsest topology). But I know it's common parlance in this context.

(I mistakenly wrote "initial topology" earlier when I meant "final topology".)

Robby955 · 2026-06-20T19:02:43Z

closing, see related AI policy discussions, thanks

Add CW complex trait to S25, S139, S158, S168, S176, S198, S210, S225
febdf4b

Robby955 marked this pull request as ready for review June 20, 2026 03:29