Skip to content

Classical CW bridge support

Mathlib has two CW-complex APIs: characteristic maps and skeleta in the classical point-set API, and categorical cell attachments in the abstract API. These nodes build only the successor-stage bridge required by Hatcher's Proposition 1.26(c).

Formalization progress
1 definition · 2 results
3 fully proved

Cell-attachment bridge

Definition1Classical and standard cells have isomorphic attaching arrows#✓fully proved

Compare the sup-norm disk-boundary inclusion used by Mathlib's classical characteristic maps with the ULifted L2 disk-boundary inclusion used by TopCat.RelativeCWComplex.basicCell.

Intended main artifact:

noncomputable def Hatcher.ClassicalCW.classicalCellArrowIso (n : ℕ) :
    Arrow.mk (Hatcher.ClassicalCW.classicalDiskBoundaryInclusion.{u} n) ≅
      Arrow.mk (TopCat.RelativeCWComplex.basicCell.{u} n ())

Define the universe-lifted classical disk, boundary, and inclusion as supporting interfaces. Use WithLp.linearEquiv for the ambient topological linear equivalence and exists_homeomorph_image_interior_closure_frontier_eq_unitBall for radial gauge rescaling. Restrict the result to the unit closed balls and spheres, then prove that the two restrictions commute with inclusion. The construction must include n = 0; a linear homeomorphism alone is insufficient because it need not preserve the two unit spheres.

Sources
Dependencies
Used byTheorem 2 (A successor classical skeleton has the cell-attachment quotient topology) · Definition 2 (Classical skeleton inclusions are abstract cell attachments)
Theorem2A successor classical skeleton has the cell-attachment quotient topology#✓fully proved

Assemble the inclusion of skeletonLT C n and the restricted characteristic maps of all classical n-cells into the joint map onto skeletonLT C (n + 1).

Intended main artifact:

theorem Hatcher.ClassicalCW.skeletonLTStepJointMap_isQuotient
    {X : Type u} [TopologicalSpace X] [T2Space X]
    (C : Set X) {D : Set X} [Topology.RelCWComplex C D] (n : ℕ) :
    Topology.IsQuotientMap
      (Hatcher.ClassicalCW.skeletonLTStepJointMap C n)

The domain is the sum of the old skeleton and the sigma type of closed sup-norm balls indexed by Topology.RelCWComplex.cell C n. Also expose the coproduct boundary and closed-cell cofans, their commuting square, and a successor-stage descent map with simp lemmas on the old skeleton and each cell.

Prove surjectivity from skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ. Prove the coinducing direction using the inherited CW structure on the successor skeleton, RelCWComplex.closed, and closedness of compact closed-cell images in the Hausdorff ambient space. The underlying set-level pushout and its compatibility with the attaching identifications are internal lemmas of this node.

Sources
Dependencies
Statement usesDefinition 1 (Classical and standard cells have isomorphic attaching arrows)
Used byDefinition 2 (Classical skeleton inclusions are abstract cell attachments)

Compactness and connectivity

Theorem1Compact subsets lie in a bounded skeleton#✓fully proved

Derive the finite-dimensional form of Hatcher's Appendix Proposition A.1: every compact subset of a classical CW complex is contained in one finite skeleton.

Intended main artifact:

theorem Hatcher.compact_subset_skeleton
    {X : Type u} [TopologicalSpace X] [T2Space X]
    {C K : Set X} [Topology.CWComplex C]
    (hK : IsCompact K) (hKC : K ⊆ C) :
    ∃ n : ℕ, K ⊆ Topology.CWComplex.skeleton C n

Apply Hatcher.compact_subset_finite_subcomplex, then extract a dimension bound from CWComplex.FiniteDimensional.eventually_isEmpty_cell. Use the subcomplex cell correspondence to show that its underlying set lies in the ambient skeleton with that bound.

Sources
Dependencies
Proof usesProposition 1 (Compact subsets lie in finite subcomplexes)
Used byTheorem 47 (The 2-skeleton of a path-connected CW complex is path-connected) · Definition 56 (The 2-skeleton determines the fundamental group)

The exact conventions and upstream status are recorded in the project-authored implementation specification.