Hatcher's auxiliary cell-attachment cover
Hatcher proves Proposition 1.26 by enlarging an indexed cell attachment with a shared spine and one strip per cell. The enlargement retracts onto the original attachment, while the strips turn the separate cone neighborhoods into one contractible member of a binary open cover.
For attaching maps f j : S j → X, chosen boundary points s₀ j, a common
basepoint x₀ : X, and paths γ j : Path x₀ (f j (s₀ j)), construct
Hatcher's auxiliary space Z.
Intended artifact: Hatcher.VanKampen.AuxiliaryCellAttachment. Give Z as an
explicit quotient containing the indexed cone attachment, a common interval
spine, and one square I × I per cell. Glue each square's bottom edge along
γ j, its left edge to the common spine, and its right edge to a fixed
truncated radial segment in the j-th cone; leave the top edge free. Expose
continuous maps for the attachment, base, spine, and strips, together with the
four boundary equations. The radial segment must avoid the cone apex so that
the apex can serve as Hatcher's removed point in the later cover.
For Hatcher's auxiliary space Z, construct a strong deformation retraction
onto the canonical copy of the indexed cone attachment. On every added square,
collapse the square onto its bottom and right edges while fixing those edges;
fix the indexed attachment throughout.
Intended artifact:
Hatcher.VanKampen.AuxiliaryCellAttachment.attachmentStrongDeformationRetract.
The module must also record that the inclusion of X through the indexed
attachment agrees with the direct base map into Z.
Dependencies
Assume the cell-index type is nonempty. In the strip-enlarged attachment,
define the base-side member by omitting every cone apex and the upper member by
omitting the canonical copy of X, using saturated height inequalities in the
quotient model. Prove that the two sets are open and cover Z, and construct a
common basepoint on the shared spine together with the path-connectedness data
needed by binary van Kampen.
Intended artifact:
Hatcher.VanKampen.AuxiliaryCellAttachment.isOpenCover_base_upper.
The same module should expose baseCover, upperCover, their inclusions, and
the chosen overlap basepoint. It does not yet prove either deformation
retraction or calculate the overlap fundamental group.
Dependencies
Construct a strong deformation retraction from the base-side member of
Hatcher's auxiliary binary cover onto the canonical copy of X. The homotopy
first collapses the added strips toward their attached bottom edges and then
pushes all positive-height cone points to their attaching points, while fixing
X throughout.
Intended artifact:
Hatcher.VanKampen.AuxiliaryCellAttachment.baseCoverStrongDeformationRetract.
Dependencies
For a nonempty family of cells, prove that the upper member of Hatcher's auxiliary cover is contractible. Contract each truncated cone neighborhood through its attached strip to the common spine, then contract that spine to the chosen overlap basepoint. The construction must remain continuous for an arbitrary index type and must not identify the distinct cone apices in the ambient attachment.
Intended artifact:
Hatcher.VanKampen.AuxiliaryCellAttachment.contractibleSpace_upperCover.
Dependencies
Let z₀ be the common basepoint chosen on the spine of Hatcher's auxiliary
cover. Construct the canonical path in the base-side member from z₀ to the
image of x₀, and prove that the base-side retraction sends its endpoint to
x₀ and its path class to the corresponding basepoint-change isomorphism.
Intended main artifact:
Hatcher.VanKampen.AuxiliaryCellAttachment.basepointPath. The same module must
expose the endpoint, retraction, and induced fundamental-group equations needed
to compare the binary-cover calculation at z₀ with
FundamentalGroup X x₀. This records Hatcher's path h explicitly rather than
requiring the two basepoints to be definitionally equal.
Cover the overlap of Hatcher's two auxiliary members by sets indexed by the
attached cells. The j-th member retains the common spine and strip system and
the punctured j-th cell, while omitting the interiors of the other cells.
Prove that these sets are open in the overlap, cover it, contain the chosen
basepoint, and have the path-connected pairwise intersections required for the
surjective clause of van Kampen.
Intended artifact:
Hatcher.VanKampen.AuxiliaryCellAttachment.isOpenCover_intersectionPieces.
The statement assumes a nonempty cell-index type and carries the exact
basepoint membership and path-connectedness witnesses consumed by
Hatcher.VanKampen.coverMap_surjective.
For every attached n-cell, construct a based homotopy equivalence from the
corresponding member of the auxiliary overlap cover to
TopCat.diskBoundary n. Its whisker runs from the common overlap basepoint
through the shared spine and strip to the selected boundary point; after that
whisker is collapsed, the remaining punctured cell retracts radially onto its
boundary sphere.
Intended artifact:
Hatcher.VanKampen.AuxiliaryCellAttachment.intersectionPieceHomotopyEquivBoundary.
This equivalence supplies the higher-dimensional triviality argument. Its
compatibility with the original attaching maps is a separate two-dimensional
node.
Dependencies
For a family of attached 2-cells, compare the meridian supplied by each
auxiliary overlap piece with the original attaching loop. After applying the
base-side retraction and changing basepoint along the canonical spine path,
the induced element of FundamentalGroup X x₀ is the attaching map applied to
the standard generator of TopCat.diskBoundary 2 and conjugated along the
chosen path γ j.
Intended artifact:
Hatcher.VanKampen.AuxiliaryCellAttachment.intersectionMeridian_eq_attachingLoop.
State the equality with all basepoint transports visible. The result must be
strong enough to identify the normal closure of the overlap image with the
normal closure of Hatcher's transported attaching loops.
Dependencies
The construction assumes a nonempty cell family. Empty attachments are handled by the separate isomorphism node in the parent support chapter.