(Relative) CW complex is T2

Stream: maths

[Robert Maxton]

I've been trying to formalize Allen Hatcher's proof that CW complexes are Hausdorff. He begins by outlining a method (which I have implemented and called mkNhd) of generating open neighborhoods of some set $A$ in a CW complex $X$ by induction on skeleta, given a function (ε : (n : ℕ) → (j : 𝓔.Cells n) → ℝ that parameterizes the Hausdorff distance the preimage of the constructed neighborhood in each open cell is allowed to be from the preimage of $A$. Then, now working with two mkNhds on $A, B$ simultaneously, he shows that given that at step n the two constructions are disjoint, there is a positive distance between the constructions and between each construction and the opposite base set $A, B$, and then concludes that it is possible to choose an ε so that the two constructions remain disjoint.

But that skips a step at the end: we need to know something about how mkNhd varies with respect to ε in order to say that "there exists some ε that makes the constructed neighborhoods small enough". We need a bound on, say, the Hausdorff distance between the constructed set and its base set, or we need that mkNhd is continuous, or something similar. But by inspection of Hatcher's method, the 'tight' bound on the Hausdorff distance turns out to be a complicated expression involving not just the dimension of the cell, but the value of ε at every cell its boundary intersects; loosening that bound to reference, say, iSup ε, breaks the induction because now you might have to reselect all previous choices of ε values in order to make the next step work out; and I have no idea how to begin to putting a topology on Set X so that I can even talk about continuous maps C((n : ℕ) → (j : 𝓔.Cells n) → ℝ, Set X).

Does anyone see either

• a way to salvage this specific proof, or
• a different, more convenient way of proving T2Space

I can work with? Or should I just leave this as a todo/proof wanted?

[Robert Maxton]

(I suppose I could just figure out how to work with said 'complicated expression', but even writing it down seems quite unpleasant and working with it is likely to be much worse, so I'm still in the market for alternative approaches.)

[Joël Riou]

This is a very technical matter. Another approach using more general topology theory is due to Ernest Michael https://ncatlab.org/nlab/show/colimits+of+paracompact+Hausdorff+spaces#ColimitsOfSequencesOfParacompacta