Relative CW complexes on Hausdorff spaces are Hausdorff #
Mathlib's categorical relative CW complex c : TopCat.RelativeCWComplex f, for a morphism
f : X ⟶ Y of TopCat, presents Y as the colimit of a sequence of spaces starting at X, each
obtained from the previous one by attaching disks along their boundary spheres. This file proves
that Y is Hausdorff when X is (TopCat.RelativeCWComplex.t2Space); in particular a CW complex
in this sense is Hausdorff (TopCat.CWComplex.t2Space). Mathlib's theory of classical CW
complexes assumes a Hausdorff ambient space, so this is needed to read a classical CW structure off
a categorical one.
The proof extends open sets cell by cell. The inclusion of the boundary sphere of a disk extends
disjoint open sets in the sense of TauCeti.TopCat.extendsDisjointOpens: an open subset U of the
sphere extends to the open cone {x | 1 / 2 < ‖x‖ ∧ x / ‖x‖ ∈ U}
(TauCeti.TopCat.extendsDisjointOpens_diskBoundaryInclusion). Hence so does every map between
the stages of the complex, and every map from a stage to Y. Two points of Y lie in a common
stage, so they are separated by open sets once that stage is Hausdorff. A stage obtained by
attaching cells to a Hausdorff space is Hausdorff (HomotopicalAlgebra.AttachCells.t2Space): two
points of the old space are separated by extending open sets, and a point of an open cell is
separated from the other points inside the disks, which are regular.
The statements hold for any relative cell complex in TopCat whose basic cells are closed
embeddings extending disjoint open sets into regular Hausdorff spaces
(HomotopicalAlgebra.RelativeCellComplex.t2Space).
Implementation notes #
The cells attached at each step are indexed by a type in the universe of the spaces, as they are
for TopCat.RelativeCWComplex, so that the coproduct of the attached disks is identified with
their disjoint union Σ i, B i (TopCat.sigmaCofanIsColimit), which is regular by
Sigma.regularSpace.
References #
- A. Hatcher, Algebraic Topology,
Appendix: the neighbourhoods
N_ε(A)of subsets of a cell complex, built cell by cell by radial extension, and Proposition A.3 that cell complexes are normal. - R. Fritsch and R. Piccinini, Cellular Structures in Topology, Cambridge University Press, 1990, for the categorical definition.
The inclusion ∂𝔻 n ⟶ 𝔻 n of the boundary sphere of the disk extends disjoint open sets: an
open subset U of the sphere is the trace of the open cone {x | 1 / 2 < ‖x‖ ∧ x / ‖x‖ ∈ U},
and the cones over disjoint sets are disjoint (TauCeti.TopCat.extendsDisjointOpens_of_continuousOn
with the radial projection).
Attaching cells to a Hausdorff space gives a Hausdorff space, provided the cells are closed embeddings into regular Hausdorff spaces which extend disjoint open sets.
A relative cell complex f : X ⟶ Y in TopCat on a Hausdorff space X has a Hausdorff
target Y, provided its basic cells are closed embeddings into regular Hausdorff spaces which
extend disjoint open sets.
A relative CW complex on a Hausdorff space is Hausdorff. If f : X ⟶ Y is a relative CW
complex in Mathlib's categorical sense and X is Hausdorff, then so is Y.
A CW complex is Hausdorff.