Weakly contractible spaces initial PR

properties/P000240.md

@@ -0,0 +1,28 @@
+---
+uid: P000240
+name: CW complex
+refs:
+  - wikipedia: CW complex
+    name: CW complex on Wikipedia
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+$X$ has a chain of subspaces $\empty = X_{-1}\subseteq X_0\subseteq X_1 \subseteq \dots$, such that:
+
+- $X_{n+1}$ can be obtained from $X_n$ by attaching $(n+1)$-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$.
+
+Here *attaching (n+1)-cells* means that there is a discrete space $J$ and for every $j \in J$ a continuous map $f_j:\partial D^{n+1} \to X_n$ such that $X_{n+1}$ is homeomorph to the quotient $(X_n \sqcup (J \times D^{n+1})) / \sim$, where $\sim$ is the equivalence relation generated by $(j,x)\sim f_j(x)$ for all $x \in J \times \partial D^{n+1}$.
+
+Here $D^n$ is the closed disk in $n$-dimensions and $\partial D^0 := \emptyset$.
+
+*Note:* In standard usage, a CW complex is a topological space together with a chain of subspaces as above (this is i.e. necessary to define cellular maps).
+However, we are only concerned with the underlying topological space.
+
+For an alternative, categorical (and more modern) definition, see <https://ncatlab.org/nlab/show/CW+complex>.
+
+----
+#### Meta-properties
+
+- This property is preserved by arbitrary disjoint unions.

properties/P000241.md

@@ -0,0 +1,21 @@
+---
+uid: P000241
+name: Weakly contractible
+aliases:
+  - Homotopically trivial
+refs:
+  - wikipedia: Weakly_contractible_space
+    name: Weakly contractible space on Wikipedia
+  - wikipedia: Homotopy_group
+    name: Homotopy group on Wikipedia
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+A nonempty, {P37} space for which all [homotopy groups](https://en.wikipedia.org/wiki/Homotopy_group) are trivial. Equivalently, the space is weakly homotopy equivalent to {S162}. 
+
+----
+#### Meta-properties
+
+- This property is preserved by homotopy equivalences.
+- This property is preserved by finite products. (See Proposition 4.2 in {{zb:1044.55001}})

theorems/T000883.md

@@ -0,0 +1,12 @@
+---
+uid: T000883
+if:
+  P000240: true
+then:
+  P000067: true
+refs:
+  - zb: "0207.21704"
+    name: The Topology of CW Complexes (Lundell, Weingram)
+---
+
+See Proposition 4.3 in {{zb:0207.21704}}, where "perfectly normal" is defined as {P67}.

theorems/T000884.md

@@ -0,0 +1,12 @@
+---
+uid: T000884
+if:
+  P000240: true
+then:
+  P000223: true
+refs:
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+See Proposition A.4 in {{zb:1044.55001}}.

theorems/T000885.md

@@ -0,0 +1,12 @@
+---
+uid: T000885
+if:
+  P000240: true
+then:
+  P000030: true
+refs:
+  - zb: "0837.55001"
+    name: Cellular structures in topology (Fritsch,Piccinini)
+---
+
+See Theorem 1.3.5 in {{zb:0837.55001}}.

theorems/T000886.md

@@ -0,0 +1,9 @@
+---
+uid: T000886
+if:
+  P000240: true
+then:
+  P000141: true
+---
+
+See Proposition 3.3 in <https://ncatlab.org/nlab/show/CW+complex>.

theorems/T000900.md

@@ -0,0 +1,9 @@
+---
+uid: T000900
+if:
+  P000241: true
+then:
+  P000037: true
+---
+
+By definition.

theorems/T000901.md

@@ -0,0 +1,9 @@
+---
+uid: T000901
+if:
+  P000241: true
+then:
+  P000137: false
+---
+
+By definition.

theorems/T000902.md

@@ -0,0 +1,9 @@
+---
+uid: T000902
+if:
+  P000199: true
+then:
+  P000241: false
+---
+
+Follows since any homotopy equivalence is also a weak homotopy equivalence.

theorems/T000903.md

@@ -0,0 +1,9 @@
+---
+uid: T000903
+if:
+  P000241: true
+then:
+  P000200: false
+---
+
+By definition, since the first homotopy group is the fundamental group.

theorems/T000904.md

@@ -0,0 +1,16 @@
+---
+uid: T000904
+if:
+  and:
+  - P000240: true
+  - P000241: true
+then:
+  P000199: false
+refs:
+  - wikipedia: Whitehead_theorem
+    name: Whitehead theorem on Wikipedia
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+Since {S162|P240}, $X$ is homotopy equivalent to the singleton by the [Whitehead theorem](https://en.wikipedia.org/wiki/Whitehead_theorem).