Skip to content

Appendix

Hatcher's appendix (pages 519–539). Most of the appendix remains mapped and explicitly deferred. The Proposition A.1 prerequisite used by §1.2 and the bounded successor-stage bridge between Mathlib's two CW-complex APIs are formalized. Proposition A.5 is formalized in five complete regular-neighborhood leaves supporting Corollary 2.24.

The point-set facts the main text uses without proving: the topology of cell complexes, including that CW complexes are normal, locally contractible, and compactly generated; the compact-open topology and the exponential law Map(X × Y, Z) ≅ Map(X, Map(Y, Z)); the homotopy extension property for CW pairs; and simplicial CW structures.

Mathlib covers part of this already. ContinuousMap.compactOpen and the currying results are in Mathlib/Topology/CompactOpen.lean, and LocallyContractibleSpace is in Mathlib/Topology/Homotopy/LocallyContractible.lean. The CW-specific separation and homotopy-extension facts are not.

This chapter is mapped so that prerequisites discovered while decomposing the main chapters have a home rather than being invented inline.

Formalization progress
1 definition · 1 result
2 fully proved

CW-complex prerequisites

Proposition1Compact subsets lie in finite subcomplexes#✓fully proved

Hatcher, Proposition A.1 (page 520). Every compact subspace of a CW complex is contained in a finite subcomplex.

Intended artifact: Hatcher.compact_subset_finite_subcomplex.

State the result against Mathlib's classical Topology.CWComplex API: for a compact subset K of a CW complex, produce a CWComplex.Subcomplex containing K whose inherited CW structure satisfies CWComplex.Finite. The ambient space is assumed Hausdorff (T2Space), as required by Mathlib's classical subcomplex and closed-cell API.

Formalized in Hatcher/Appendix/CompactSubspaceFiniteSubcomplex.lean. The proof first shows that a compact subset meets only finitely many open cells, then closes this finite family under cell frontiers and constructs the resulting finite subcomplex.

The §1.2 proof that the 2-skeleton determines π₁ uses this twice. The separate bounded-skeleton corollary packages the exact form consumed there: a loop image, or the image of its nullhomotopy, lies in one finite skeleton.

Sources
Dependencies
Used byTheorem 1 (Compact subsets lie in a bounded skeleton)
Definition2Classical skeleton inclusions are abstract cell attachments#✓fully proved

For a classical Mathlib CW complex, package the inclusion from one strict skeleton to the next as a standard categorical cell attachment.

Intended main artifact:

noncomputable def Hatcher.ClassicalCW.skeletonLTInclusion_attachCells
    {X : Type u} [TopologicalSpace X] [T2Space X]
    (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (n : ℕ) :
    HomotopicalAlgebra.AttachCells.{u}
      (TopCat.RelativeCWComplex.basicCell.{u} n)
      (Hatcher.ClassicalCW.skeletonLTInclusion C n)

First turn the successor-stage quotient theorem into a TopCat pushout for the coproduct of classical sup-norm cells. Then transport the cell family along classicalCellArrowIso with AttachCells.reindexCellTypes. Also expose the wrapper Hatcher.ClassicalCW.skeletonInclusion_attachCells C n, whose cells have dimension n + 1 and whose underlying map is CWComplex.skeleton C n → CWComplex.skeleton C (n + 1).

This is the one-stage bridge needed by Hatcher's Proposition 1.26(c). It does not construct a full abstract CW structure from a classical one. Mathlib documents that broader comparison as a TODO and provides no bridge in the pinned revision.

Sources
Dependencies
Statement usesDefinition 1 (Classical and standard cells have isomorphic attaching arrows) · Theorem 2 (A successor classical skeleton has the cell-attachment quotient topology)
Used byTheorem 47 (The 2-skeleton of a path-connected CW complex is path-connected) · Definition 54 (Finite skeleta above dimension two have the same fundamental group)

Sources