Cell-attachment support
These nodes isolate the reusable algebra, elementary circle geometry, and the first point-set construction around Hatcher's cell-attachment applications.
Point-set geometry
For a map f : S → X, construct the point-set quotient of X ⊔ {*} ⊔ (S × I)
that collapses S × {0} to the explicit cone apex and glues S × {1} to X
through f. Later deformation results will require f to be continuous; the
quotient and its open cover do not.
The subsets consisting respectively of the canonical image of X with all
positive-height cone points, and the apex with all subunit-height cone points,
are open and cover the quotient. This is formalized by
Hatcher.VanKampen.ConeAttachment.isOpenCover_lower_upper; the module also
provides the endpoint quotient identities and restricted quotient maps needed
to descend the later deformation homotopies.
This node deliberately handles one augmented cone. It does not yet model an
arbitrary family of attached cells: that construction needs one apex per cell,
the deformation retractions, and a comparison with Mathlib's
HomotopicalAlgebra.AttachCells pushout.
Dependencies
For attaching maps f j : S j → X, construct the quotient of X with one
cone on each S j. Each index has its own apex, so different cells do not
acquire an artificial common center. When the index type is empty, the
construction is homeomorphic to X with no extra point.
The base with all positive-height cone points and the family of apex
neighborhoods with all subunit-height points are open and cover the quotient.
This is formalized by
Hatcher.VanKampen.IndexedConeAttachment.isOpenCover_lower_upper; the empty
case is Hatcher.VanKampen.IndexedConeAttachment.emptyIndexHomeomorph.
The upper member is generally a disjoint union of truncated cones, hence need not be connected or contractible. Hatcher's auxiliary cover must still connect these pieces before the binary van Kampen theorem applies.
Dependencies
For a continuous attaching map f : S → X, the open member consisting of the
canonical image of X together with the positive-height cone points strongly
deformation-retracts onto X.
Formalized as
Hatcher.VanKampen.ConeAttachment.lowerStrongDeformationRetract. The homotopy
pushes every positive cylinder height linearly toward one, where the boundary
is glued to X, and fixes the image of X throughout. The module also exposes
the inclusion and retraction maps and proves their composite is the identity.
For a continuous attaching map f : S → X, the open member consisting of the
cone apex and all subunit-height cylinder points is contractible.
Formalized as
Hatcher.VanKampen.ConeAttachment.contractibleSpace_upperCover. Its explicit
pointed contraction pushes every cylinder height linearly to zero and fixes
the cone apex throughout.
For the standard two-set cover of a single cone attachment, the intersection
is homeomorphic to the open cylinder S × (0,1) and hence homotopy equivalent
to the attaching space S.
The homeomorphism is
Hatcher.VanKampen.ConeAttachment.interiorCylinderHomeomorphCoverIntersection;
the source-facing homotopy equivalence is
Hatcher.VanKampen.ConeAttachment.coverIntersectionHomotopyEquivBase. The
proof restricts the quotient map to the open intersection and observes that no
endpoint identifications remain there.
No continuity hypothesis on the attaching function is needed for this identification. Continuity enters when the cover pieces are compared with the base space and the full attachment pushout.
The single-cone quotient attached to Mathlib's exact TopCat.diskBoundary n
by the identity map is homeomorphic to TopCat.disk n.
Formalized as Hatcher.VanKampen.ConeAttachment.diskHomeomorph. The proof
uses the radial map: retained boundary points have radius one, the cone apex
maps to the origin, and a cylinder point (x,t) maps to t • x. Its kernel is
exactly the cone-attachment relation.
The companion theorem
Hatcher.VanKampen.ConeAttachment.diskHomeomorph_base_eq_diskBoundaryInclusion
shows that the homeomorphism carries the retained boundary to Mathlib's
TopCat.diskBoundaryInclusion n. Thus this is a comparison with the same
boundary and disk objects used by TopCat.RelativeCWComplex.basicCell, not a
homeomorphic substitute with an unrecorded change of model.
Dependencies
For a continuous map f : S → X, the explicit single-cone attachment is the
pushout in TopCat of f and the retained-boundary inclusion
S → ConeAttachment id.
Formalized as
Hatcher.VanKampen.ConeAttachment.isPushout_coneAttachment. The proof builds
the universal map out of the quotient and proves uniqueness on the base, apex,
and cylinder representatives.
The same module packages this square as
Hatcher.VanKampen.ConeAttachment.attachCells_coneAttachment, a one-cell
HomotopicalAlgebra.AttachCells structure for the retained-cone cell type.
The separate cone-to-disk homeomorphism identifies that cell geometrically
with Mathlib's standard disk; the
single standard-cell bridge transports this
structure to TopCat.RelativeCWComplex.basicCell.
For a continuous attaching map from TopCat.diskBoundary n into X, the
canonical inclusion of X into the cone quotient carries a one-cell
HomotopicalAlgebra.AttachCells structure for Mathlib's exact
TopCat.RelativeCWComplex.basicCell n family.
Formalized as Hatcher.VanKampen.ConeAttachment.attachCells_basicCell. The
proof first identifies the retained cone with TopCat.disk n, including its
boundary map, then transports the explicit cone pushout along that arrow
isomorphism using Mathlib's AttachCells.reindexCellTypes.
This closes the representation bridge for one disk. The formalized downstream nodes extend it to arbitrary indexed families and Hatcher's connected auxiliary cover.
Dependencies
For a family of continuous attaching maps f j : S j → X, bundle the maps
from the topological coproduct Σ j, S j to X and to the coproduct of the
retained cones Σ j, ConeAttachment (id : S j → S j). The explicit indexed
cone quotient is their pushout in TopCat.
Intended artifact:
Hatcher.VanKampen.IndexedConeAttachment.isPushout_indexedConeAttachment.
The same module should expose the four maps in this square and the resulting
HomotopicalAlgebra.AttachCells structure for the indexed retained-cone cell
family. Use TopCat.sigmaCofan and TopCat.sigmaCofanIsColimit, and keep the
index and space universes equal in this first interface rather than hiding a
resizing assumption.
Sources
Dependencies
Fix a dimension n. For a family of continuous maps from
TopCat.diskBoundary n to X, equip the canonical base inclusion into the
indexed cone quotient with a HomotopicalAlgebra.AttachCells structure for
Mathlib's exact family TopCat.RelativeCWComplex.basicCell n.
Intended artifact:
Hatcher.VanKampen.IndexedConeAttachment.attachCells_basicCell.
It should first package the indexed pushout with one retained cone per index,
then transport every cell arrow through the already formalized cone-to-disk
homeomorphism. The initial interface uses AttachCells.{u} with the cell index
in Type u; support for a separately sized index type is a later resizing
problem, not an implicit assumption here.
Dependencies
Let c : HomotopicalAlgebra.AttachCells.{u}
(TopCat.RelativeCWComplex.basicCell n) f. Define the attaching map of its cell
i : c.ι by following the i-th boundary coproduct injection with c.g₁.
Construct an isomorphism from the target of f to the explicit indexed cone
attachment of these maps.
Intended main artifact: Hatcher.VanKampen.CellAttachment.modelIso.
The module must also prove that this isomorphism commutes with the base map and
with every cell inclusion:
@[reassoc] theorem f_modelIso_hom :
f ≫ (modelIso c).hom = IndexedConeAttachment.baseHom (attachingMap c)
@[reassoc] theorem cell_modelIso_hom (i : c.ι) :
c.cell i ≫ (modelIso c).hom = modelDiskHom c i
These equations preserve the maps needed later to identify the two-cell relations, rather than recording only an unpointed homeomorphism of targets.
Dependencies
For c : HomotopicalAlgebra.AttachCells.{u}
(TopCat.RelativeCWComplex.basicCell n) f with an empty cell-index type, show
that the attachment map f is an isomorphism in TopCat.
Intended artifact: Hatcher.VanKampen.CellAttachment.targetIsoOfIsEmpty.
Compose the abstract-to-indexed model isomorphism with the homeomorphism from
an empty indexed cone attachment to its base. This is the degenerate branch of
Proposition 1.26; it must not be handled by adding a dummy apex to Hatcher's
nonempty connected cover.
Sources
Attaching an arbitrary family of cells of one fixed dimension greater than one does not merge path components of the source.
Intended main artifact:
theorem Hatcher.joined_iff_of_attachCells_of_one_lt
{n : ℕ} {X Y : TopCat.{u}} {f : X ⟶ Y}
(c : HomotopicalAlgebra.AttachCells.{u}
(TopCat.RelativeCWComplex.basicCell.{u} n) f)
(hn : 1 < n) (x y : X) :
Joined (f x) (f y) ↔ Joined x y
Also provide Hatcher.pathConnectedSpace_of_attachCells_of_two_lt: if X is
path-connected and 2 < n, then Y is path-connected. No finiteness
assumption on the cell index is allowed.
Transport the target to the explicit indexed-cone model. Radial paths join
every disk point to its nonempty boundary, while path-connectedness of
TopCat.diskBoundary n for 1 < n shows that one attached disk cannot join
distinct source components. Establish the reverse implication for paths whose
endpoints lie in the base, not only the easier forward path-connectedness
corollary. Treat an empty cell family through the existing target isomorphism.
Dependencies
Supply the path-connectedness instance required before iterating the higher-cell fundamental-group theorem from the classical 2-skeleton.
Intended main artifact:
theorem Hatcher.ClassicalCW.pathConnectedSpace_twoSkeleton
{X : Type u} [TopologicalSpace X] [T2Space X]
(C : Set X) [Topology.CWComplex C] [PathConnectedSpace C] :
PathConnectedSpace (Topology.CWComplex.skeleton C (2 : ℕ∞))
For two points of the 2-skeleton, choose a path between them in C. Its image
is compact, hence lies in a bounded skeleton. Work downward through the
finitely many higher dimensions. At each step, use the classical attachment
bridge and joined_iff_of_attachCells_of_one_lt to reflect joinedness across
the successor-skeleton inclusion. This proves the instance from ambient
path-connectedness; the theorem must not assume the 2-skeleton is
path-connected.
Sources
Dependencies
The raw indexed quotient has one apex per cell, so its upper member is generally disconnected. Hatcher repairs this by adjoining a shared spine and one strip per cell. The strip-enlarged point-set construction is organized in Hatcher's auxiliary cell-attachment cover. The separate two-disk boundary comparison fixes the circle parameterization used by the two-cell relation calculation.
The finite-stage constructors, pointed-wedge interfaces, and relator family needed for Corollary 1.28 are formalized in presentation-complex support.
Binary-cover algebra
Let two path-connected open sets cover X, and suppose the second member has
trivial fundamental group. Then π₁(X) is the quotient of the first member's
fundamental group by the normal closure of the image of the intersection
group.
Formalized as
Hatcher.VanKampen.binaryCoverLeftQuotientEquivFundamentalGroupOfSubsingleton
in Hatcher/VanKampen/CellAttachmentAlgebra.lean. Its companion formulas show
that the quotient map followed by this equivalence is exactly the homomorphism
induced by inclusion of the first cover member.
The module also proves the underlying group-theoretic result: a binary pushout whose second factor is subsingleton is the quotient of its first factor by the normal closure of the amalgamating map's image.
This is the algebraic endgame of the 2-cell attachment calculation. The point-set attachment cover and the identification of the overlap generators with the attaching loops remain geometric prerequisites.
Dependencies
Let two path-connected open sets cover Y. Suppose the second member is
contractible, their intersection is simply connected, and the first member
strongly deformation retracts onto the image of a space A. Then inclusion
induces an equivalence π₁(A) ≃* π₁(Y).
Formalized as
Hatcher.VanKampen.fundamentalGroupEquivOfBinaryCoverRetraction in
Hatcher/VanKampen/CellAttachmentAlgebra.lean. The same module proves the
underlying algebraic fact that a binary group pushout with trivial
amalgamating group and trivial second factor is equivalent to its first
factor, and records that the resulting equivalence is induced by inclusion.
This is the algebraic endgame of the higher-cell attachment argument. The point-set construction of Hatcher's auxiliary cover and the proof that its intersection is simply connected remain separate geometric prerequisites.
Circle input
The standard basepoint 1 ∈ S¹ has an open neighborhood that strongly
contracts to 1. Consequently the pointed-wedge theorem applies to arbitrary
families of circles without an additional geometric hypothesis.
Formalized as Hatcher.Circle.wellPointedAt_one in
Hatcher/Circle/WellPointed.lean. The proof uses the stereographic chart
centered at -1, which identifies its open source with a real topological
vector space and sends 1 to the origin. Scalar contraction in the chart
fixes that origin throughout.
The same module exposes Hatcher.WellPointedAt.of_open_homeomorph_zero, a
general criterion for proving that a point is well-pointed from such a chart.
Dependencies
For a natural number n, let dₙ : S¹ → S¹ be the map z ↦ zⁿ. The
induced homomorphism on fundamental groups sends the chosen degree-one loop
class to the degree-n loop class.
Formalized as Hatcher.Circle.mapOfEq_degreeMap_degreeLoopClass_one in
Hatcher/VanKampen/CyclicPresentationAlgebra.lean. The stronger path-level
formula degreeMap_map_loopOfInt shows that dₙ sends every degree-m loop
to the degree-n m loop. The sign is positive for the project's
counterclockwise generator.
This is the attaching-map compatibility needed by the cyclic presentation complex. It does not construct that cell attachment.
Dependencies
For a natural number n, quotient π₁(S¹, 1) by the normal closure of the
class of the degree-n loop. The resulting group is isomorphic to
Multiplicative (ZMod n).
Formalized as Hatcher.cyclicPresentationQuotientEquiv in
Hatcher/VanKampen/CyclicPresentationAlgebra.lean. The definition
Hatcher.Circle.degreeLoopClass names the relator, and the companion
application theorems record that the quotient equivalence is winding number
reduced modulo n.
This is the complete algebraic endgame of Hatcher's cyclic presentation complex calculation. It does not construct the topological adjunction space or prove that attaching a 2-cell imposes this relation.
Dependencies
The family open-cover construction and attaching-sphere analysis are packaged in the parent Van Kampen roadmap, where they feed the now-formalized 2-cell and higher-cell attachment theorems.
Additional formalization targets
Construct a basepoint-preserving homeomorphism from Mathlib's
TopCat.diskBoundary 2 to _root_.Circle, using the standard linear
identification of two-dimensional Euclidean space with the complex plane. The
distinguished boundary point is the ULift of the unit vector (1, 0), and
the homeomorphism must send it to 1 : Circle.
Intended artifact: Hatcher.diskBoundaryTwoHomeomorphCircle. The module should
also expose the loop on TopCat.diskBoundary 2 obtained by transporting
Hatcher's standard once-around loop, so an attaching map has a canonical
fundamental-group element with the orientation used by the existing winding
number calculation.