CW-subcomplex regular neighborhoods

Hatcher's Appendix Proposition A.5 constructs an open regular neighborhood of every subcomplex of a CW complex and strongly deformation retracts that neighborhood onto the subcomplex. The construction here is deliberately narrow: it fixes one common collar width for every cell and retains the intersection identity needed for Corollary 2.24.

All five formalization leaves are complete.

Definition112Intersections of CW subcomplexes#✓fully proved

For two CWComplex.Subcomplex C objects, construct the subcomplex whose cells are those belonging to both inputs and whose carrier is their set-theoretic intersection. Expose the coercion formula

↑(Hatcher.ClassicalCW.Subcomplex.inter A B) = (A : Set X) ∩ (B : Set X)

and the corresponding cell-index formula. The main artifact is Hatcher.ClassicalCW.Subcomplex.inter.

This is topology-neutral infrastructure for the identity N(A) ∩ N(B) = N(A ∩ B) following Hatcher's Proposition A.5. The pinned Mathlib revision has a CWComplex.Subcomplex structure but no intersection or lattice operation on it.

Sources
Dependencies
Used byStructure 8 (A common regular-neighborhood system for subcomplexes) · Theorem 111 (Subcomplex decompositions admit compatible neighborhoods)
Definition113The radial collar of a cell boundary#✓fully proved

For the closed sup-norm ball used by a classical CW characteristic map, construct the fixed-width radial collar of its boundary and a deformation that slides this collar outward onto the boundary. The deformation must be stationary on the boundary and respect the radial coordinate. In the global time schedule it is the identity before its assigned interval and remains constant at its retracted endpoint after that interval.

The main artifact is Hatcher.ClassicalCW.cellBoundaryCollarDeformation. Supporting declarations record the collar set, its openness relative to the closed cell, its radial retraction, and endpoint and boundary-fixing formulas.

This is the cellwise construction used in Hatcher's proof of Proposition A.5; it does not yet descend through characteristic maps or assemble a global CW homotopy.

Sources
Dependencies
Used byStructure 8 (A common regular-neighborhood system for subcomplexes)
Structure8A common regular-neighborhood system for subcomplexes#✓fully proved

For a classical CW complex C, construct one fixed-width regular-neighborhood assignment N for all CWComplex.Subcomplex C. Package the facts that

  • N A is open in the ambient CW complex;
  • the carrier of A lies in N A, hence in its interior; and
  • N (A.inter B) = N A ∩ N B.

The main artifact is Hatcher.ClassicalCW.RegularNeighborhoodSystem. It uses the same collar width, chosen once with 0 < ε < 1, in every occurrence of N; independently chosen neighborhoods would not support the required intersection identity.

This node constructs the neighborhoods and their point-set identities. The global deformation retraction is the next node.

Sources
Prior art

The completed successor-skeleton quotient bridge records compatible quotient topology techniques, but it is not an authored mathematical prerequisite.

Dependencies
Statement usesDefinition 112 (Intersections of CW subcomplexes) · Definition 113 (The radial collar of a cell boundary)
Used byDefinition 114 (A regular neighborhood strongly deformation retracts onto its subcomplex) · Theorem 111 (Subcomplex decompositions admit compatible neighborhoods)
Definition114A regular neighborhood strongly deformation retracts onto its subcomplex#✓fully proved

Hatcher, Appendix Proposition A.5 (printed page 523). For every subcomplex A of a classical CW complex, the canonical inclusion of A into its fixed-width regular neighborhood is a strong deformation retract:

def Hatcher.ClassicalCW.regularNeighborhoodStrongDeformationRetract
    (A : CWComplex.Subcomplex C) :
    Hatcher.StrongDeformationRetract
      (regularNeighborhoodInclusion A)

Assemble the cellwise radial deformations dimension by dimension, fixing A throughout. The proof must establish continuity of the global homotopy, not merely continuity on each open cell; it may use the existing compact-subset and successor-skeleton infrastructure to justify the closed-cell-times- interval gluing step.

Sources
Prior art

The completed compact-subset and classical-skeleton bridge modules may guide the closed-cell-times-interval continuity argument, but they are not authored mathematical prerequisites of this result.

Dependencies
Statement usesStructure 8 (A common regular-neighborhood system for subcomplexes) · Structure 4 (Strong deformation retracts)
Used byTheorem 111 (Subcomplex decompositions admit compatible neighborhoods)
Theorem111Subcomplex decompositions admit compatible neighborhoods#✓fully proved

Let A and B be subcomplexes whose carriers cover a classical CW complex C. Package their regular neighborhoods U = N A and V = N B with

  • A ⊆ interior U and B ⊆ interior V;
  • strong deformation retractions U ↘ A and V ↘ B;
  • U ∩ V = N (A ∩ B); and
  • the induced strong deformation retraction U ∩ V ↘ A ∩ B.

The main artifact is Hatcher.ClassicalCW.subcomplexNeighborhoodCover. Keep this structure in a topology-neutral module so Corollary 2.24 can consume it without depending on the later Mayer–Vietoris development.

The statement includes the empty-intersection case. When A ∩ B is empty, the common neighborhood and its deformation data are empty as well.

Sources
Dependencies
Statement usesDefinition 112 (Intersections of CW subcomplexes) · Structure 8 (A common regular-neighborhood system for subcomplexes) · Definition 114 (A regular neighborhood strongly deformation retracts onto its subcomplex)
Used byCorollary 2 (Excision holds for a union of CW subcomplexes)

The implementation boundary and the continuity argument for the assembled homotopy are fixed in the project-authored implementation specification.

Formalization progress
4 definitions · 1 result
5 fully proved