Chapter 0. Some Underlying Geometric Notions
FC07 — Hatcher, Algebraic Topology.
This chapter contains 10 definitions, 4 propositions, 2 corollaries, 15 examples and 10 constructions.
Of the 41 statements checked against Lean, 11 are formalized somewhere and 30 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 30 | 73% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 7 | 17% | Mathlib states and proves it. |
| in another Lean project | 4 | 10% | Some other Lean development has it; using it means porting that code. |
| checked in total | 41 |
- Canonical source block: FC07 Hatcher, Chapter 0,
FC07-C00-U001–FC07-C00-U041, in canonical source-ID order, extracted from FC07 — Hatcher, Algebraic Topology throughagent-memory. The extraction contains exactly 41 contiguous rows. FC01–FC06 were left closed and no FC13 scratch or vault record was touched. - Project-first inspection was refreshed at repository HEAD
A=3b2239e161592472b34e02ad3b7da308f9ce7280. No project-owned declaration inLeanCategories/**owns a complete C00 source row, so noproject-existingroute is promoted. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0 and directly project-compatible. Everymathlibdeclaration promoted in the table was inspected at that exact revision. - Current upstream Mathlib was refreshed on 2026-09-06 at
H=633b366493a76df88a2bff099ed0cbf711a59ec9, Lean 4.34.0-rc2, Apache-2.0. Searches at H and in current open Mathlib PRs found ongoing classical-CW infrastructure work but no post-pin route completing the missing suspension/smash/mapping-cone, product/quotient-CW, or HEP proposition bundles. deancureton/sphere-six-complex@895c0a0661501581c34d42fea3c553d4f0ee43b1is Apache-2.0 and uses Lean 4.34.0-rc1. It contains exact general-topology implementations of strong deformation retractions, mapping cylinders/pushout homotopies, HEP, and Hatcher Cor. 0.20. Because it is not the project pin and no direct package-compatibility import test against Lean 4.33.0 was established, all promoted uses arereference-port, notpackage-import.Vilin97/lean-pool@3fc79f0a795f19fffcc59eee3efaf5faa52de3c3was inspected as a Reservoir/local reference source. Its Whitehead/HEP development has a target-specific HEP interface and supplies adjacent evidence but no stricter route than the promoted sphere-six declarations.facebookresearch/atlas-lean@34ffed396f376454c1a9b297f3fd74c5c801fb50was also checked for its deformation-retract interface; it uses Lean 4.29.0 and a noncommercial/no-training license, and no C00 row depends on it.- Indexed/search-service probes (Mathlib docs, Loogle/LeanSearch-oriented searches, Reservoir/package search, GitHub-wide Lean search, and local reference-corpus scans) were used for the remaining gaps. Generic category-theoretic cones, joins, pushouts, and homological mapping cones were not conflated with Hatcher’s topological constructions.
- Strict bundle semantics govern every row. A route must own the complete stable-ID statement. A theorem for only one clause, one example, a specialization, or a semantically adjacent object is retained as adjacent evidence but does not promote the row.
- U008 is deliberately unmatched despite Mathlib’s
CWComplex/RelCWComplexcharacteristic-map interface, skeletons, and skeleton-union theorems: the source row specifically gives the inductive discrete-0-skeleton/successive-cell-attachment construction, and no checked theorem bridges the complete source construction to the current classical-CW presentation. - U009 is likewise not inferred from
CWComplex.OneSkeletonGraph: that declaration extracts a combinatorial graph from the 1-skeleton, but the checked API does not identify an arbitrary one-dimensional CW complex with a topological graph realization as the source example states. - U015 and U016 are promoted because Mathlib’s characteristic-map and subcomplex interfaces are direct equivalent representations rather than weaker consequences: closed-ball characteristic maps restrict to homeomorphisms on open cells, and subcomplexes are closed unions of cells with an induced CW structure.
- U028 is represented exactly by the topological pushout: the underlying type pushout is explicitly the quotient of the disjoint union by the attachment relation, and
TopCat.colimit_topologyequips it with the final topology. - U036 remains unmatched even though
hasHomotopyExtensionProperty_of_relativeCWComplex_provedproves its HEP consequence. The external proof constructs an ordinary retraction of the L-shaped cylinder and explicitly does not establish the stronger deformation-retract clause bundled into Hatcher Prop. 0.16. - U040 is the exact external Cor. 0.20 theorem and returns the stronger stationary (strong) deformation retraction. U037–U039 remain unmatched because no searched declaration owns their respective quotient-collapse, homotopic-attachment, or relative-homotopy-equivalence statements in full.
- U041 remains unmatched under whole-row semantics: the external mapping-cylinder/HEP/strong-deformation-retract API supplies ingredients and directions, but no checked declaration packages both Hatcher’s iff and the common-ambient-space characterization.
N=2026-09-06marks a dated unmatched decision after project-first, P, H/current/open work, indexed search services, Reservoir/local reference sources and relevant external Lean repositories.
Definition — deformation retraction
A deformation retraction of X onto A is a continuous family f_t:X→X with f_0=id_X, f_1(X)=A, and f_t|_A=id_A for all t.
Formalized. deancureton/sphere-six-complex::SphereSixComplex/Topology/EstablishedStrongDeformationRetracts.lean::SphereSixComplex.StrongDeformationRetraction — The structure records a self-retraction with image in the specified subspace, identity on that subspace, and a homotopy from the identity to the retraction fixed pointwise on the subspace. Together retract_mem and retract_fixed give image exactly the subspace, matching Hatcher’s deformation-retraction convention.
Searched: R=895c0a0661501581c34d42fea3c553d4f0ee43b1; Apache-2.0; Lean 4.34.0-rc1
Definition/construction — mapping cylinder
For f:X→Y, the mapping cylinder M_f is (X×I)⊔Y modulo (x,1)∼f(x); it deformation retracts onto Y.
Formalized. deancureton/sphere-six-complex::SphereSixComplex/Topology/MappingCylinderGluing.lean::TopCat.MappingCylinder, TopCat.mappingCylinderBase, TopCat.cylinderZeroStrongDeformationRetract; SphereSixComplex/Topology/PushoutHomotopy.lean::TopCat.StrongDeformationRetractData.pushoutRetraction, pushoutHomotopy, inr_pushoutRetraction, inr_pushoutPaths — The mapping cylinder is the topological pushout of a cylinder endpoint and f; interval reversal identifies its zero-end convention with Hatcher’s one-end convention. The cited pushout data gives a retraction onto the target copy and a homotopy to the identity whose target branch stays fixed, so the target is a deformation retract as required.
Searched: R=895c0a0661501581c34d42fea3c553d4f0ee43b1; Apache-2.0; Lean 4.34.0-rc1
Definition — homotopy and homotopic maps
A homotopy from f_0 to f_1 is a continuous F:X×I→Y, written F(x,t)=f_t(x); maps joined by such a family are homotopic, f_0≃f_1.
Formalized. Mathlib/Topology/Homotopy/Basic.lean::ContinuousMap.Homotopy, ContinuousMap.Homotopic — Pinned Mathlib defines a homotopy as a continuous map on I × X with prescribed endpoint maps and defines Homotopic by existence of such a homotopy, exactly the source unit up to the order of product coordinates.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — retraction
A retraction onto A⊂X is a map r:X→A restricting to id_A; equivalently, viewed as X→X with image A, it satisfies r²=r.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A retraction onto A⊂X is a map r:X→A restricting to id_A; equivalently, viewed as X→X with image A, it satisfies r²=r. deancureton/sphere-six-complex::SphereSixComplex/Topology/RelativeHomotopy.lean::SphereSixComplex.DeformationRetractData.retractMap_idempotent proves the idempotence direction for a deformation retraction, but no checked route supplies the complete general retraction definition together with Hatcher’s stated equivalence with image-idempotent self-maps. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — homotopy relative to A
A homotopy f_t:X→Y is rel A when f_t|_A is independent of t.
Formalized. Mathlib/Topology/Homotopy/Basic.lean::ContinuousMap.HomotopyRel, ContinuousMap.HomotopicRel — A HomotopyRel f₀ f₁ A is a homotopy whose value on every point of A is independent of time, exactly Hatcher’s “rel A” condition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — homotopy equivalence and homotopy type
A map f:X→Y is a homotopy equivalence if some g:Y→X satisfies fg≃id_Y and gf≃id_X; then X and Y have the same homotopy type.
Formalized. Mathlib/Topology/Homotopy/Equiv.lean::ContinuousMap.HomotopyEquiv (X ≃ₕ Y) — The structure consists of continuous maps in both directions whose two composites are homotopic to the appropriate identities. Existence of this structure is precisely equality of homotopy type in the source sense.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — contractible and nullhomotopic
A space is contractible when it has the homotopy type of a point, equivalently when its identity map is homotopic to a constant map (nullhomotopic).
Formalized. Mathlib/Topology/Homotopy/Contractible.lean::ContractibleSpace, ContinuousMap.Nullhomotopic, contractible_iff_id_nullhomotopic — ContractibleSpace is defined by a homotopy equivalence with Unit, and the cited iff theorem identifies this exactly with nullhomotopy of the identity map.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition/construction — CW complex, cells, and skeleta
A CW complex is built inductively from a discrete 0-skeleton X^0 by attaching n-cells D^n along maps S{n-1}→X{n-1}; X^n is the n-skeleton and X=⋃_nX^n.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A CW complex is built inductively from a discrete 0-skeleton X^0 by attaching n-cells D^n along maps S{n-1}→X{n-1}; X^n is the n-skeleton and X=⋃_nX^n. Pinned Mathlib has Mathlib/Topology/CWComplex/Classical/Basic.lean::Topology.CWComplex, RelCWComplex.skeleton, skeleton_union_iUnion_closedCell_eq_skeleton_succ, and iUnion_skeleton_eq_complex, but its classical CW interface is characteristic-map/weak-topology based; no checked bridge realizes the source’s full inductive “discrete 0-skeleton + successive sphere-to-disk attachments” construction. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.1
A 1 dimensional cell complex X = X^{1} is what is called a graph in algebraic topology. It consists of vertices (the 0 cells) to which edges (the 1 cells) are attached. The two ends of an edge can be attached to the same vertex.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A 1 dimensional cell complex X = X^{1} is what is called a graph in algebraic topology. It consists of vertices (the 0 cells) to which edges (the 1 cells) are attached. The two ends of an edge can be attached to the same vertex. Pinned Mathlib has Mathlib/Topology/CWComplex/Classical/Graph.lean::Topology.CWComplex.OneSkeletonGraph and loop-edge lemmas, extracting the combinatorial graph of a CW 1-skeleton. The checked interface does not identify an arbitrary 1-dimensional CW complex with a topological realization of that graph, so the whole source example is not promoted. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.2
The house with two rooms, pictured earlier, has a visually obvious 2 dimensional cell complex structure. This gives the 1 skeleton X^{1}, and the 2 cells are the components of the remainder of the space, X - X^{1}.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The house with two rooms, pictured earlier, has a visually obvious 2 dimensional cell complex structure. This gives the 1 skeleton X^{1}, and the 2 cells are the components of the remainder of the space, X - X^{1}. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.3
The sphere S^{n} has the structure of a cell complex with just two cells, e^{0} and e^{n}, the n cell being attached by the constant map S^{n - 1} {→ } e^{0}. This is equivalent to regarding S^{n} as the quotient space D^{n} / ∂ D^{n}.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The sphere S^{n} has the structure of a cell complex with just two cells, e^{0} and e^{n}, the n cell being attached by the constant map S^{n - 1} {→ } e^{0}. This is equivalent to regarding S^{n} as the quotient space D^{n} / ∂ D^{n}. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.4
Real projective n space ℝP^{n} is defined to be the space of all lines through the origin in ℝ^{n + 1}. It follows by induction on n that ℝP^{n} has a cell complex structure e^{0} ∪ e^{1} ∪ … ∪ e^{n} with one cell e^{i} in each dimension i ≤ n.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Real projective n space ℝP^{n} is defined to be the space of all lines through the origin in ℝ^{n + 1}. It follows by induction on n that ℝP^{n} has a cell complex structure e^{0} ∪ e^{1} ∪ … ∪ e^{n} with one cell e^{i} in each dimension i ≤ n. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.5
Since ℝP^{n} is obtained from ℝP^{n - 1} by attaching an n cell, the infinite union {ℝ } {P }^{∞} = ⋃{n} {ℝ } {P }^{n} becomes a cell complex with one cell in each dimension. We can view ℝP^{∞} as the space of lines through the origin in ℝ^{∞} = ⋃{n} ℝ^{n}.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Since ℝP^{n} is obtained from ℝP^{n - 1} by attaching an n cell, the infinite union {ℝ } {P }^{∞} = ⋃{n} {ℝ } {P }^{n} becomes a cell complex with one cell in each dimension. We can view ℝP^{∞} as the space of lines through the origin in ℝ^{∞} = ⋃{n} ℝ^{n}. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.6
Complex projective space ℂP^n is the quotient of S^{2n+1} by scalar multiplication by S^1. It is obtained from ℂP^{n−1} by attaching one 2n-cell, hence has CW structure e0∪e2∪⋯∪e^{2n}; ℂP^∞ has one cell in every even dimension.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Complex projective space ℂP^n is the quotient of S^{2n+1} by scalar multiplication by S^1. It is obtained from ℂP^{n−1} by attaching one 2n-cell, hence has CW structure e0∪e2∪⋯∪e^{2n}; ℂP^∞ has one cell in every even dimension. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — characteristic map
Each n-cell e_α^n has a characteristic map Φ_α:D^n→X extending its attaching map and restricting to a homeomorphism int(Dn)→e_αn.
Formalized. Mathlib/Topology/CWComplex/Classical/Basic.lean::Topology.RelCWComplex.map, source_eq, continuousOn, continuousOn_symm, openCell, mapsTo — Mathlib represents each cell by a partial equivalence whose source is the open unit ball, continuous on the closed unit ball, with continuous inverse on the open cell; its sphere boundary maps into lower cells. Restricting the same map to the closed ball is the characteristic map and its open-ball restriction is a homeomorphism onto the cell.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition — subcomplex and CW pair
A subcomplex A⊂X is a closed union of cells; a pair (X,A) with A a subcomplex is a CW pair.
Formalized. Mathlib/Topology/CWComplex/Classical/Basic.lean::Topology.RelCWComplex.Subcomplex, Subcomplex.closed, Subcomplex.union; Mathlib/Topology/CWComplex/Classical/Subcomplex.lean::Topology.CWComplex.Subcomplex.instCWComplex, CWComplex.Subcomplex.union_closedCell — A Mathlib CW subcomplex is exactly a closed subspace which is a union of cells; the induced CW-complex instance supplies the pair structure. Mathlib uses the subcomplex object itself rather than introducing a separate redundant CWPair predicate.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — product CW structure
For CW complexes X,Y, the product has cells e_αm×e_βn; in general the resulting CW topology can be finer than the ordinary product topology.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For CW complexes X,Y, the product has cells e_αm×e_βn; in general the resulting CW topology can be finer than the ordinary product topology. Pinned/current Mathlib has product topology and CW cells, but no checked construction equips the product of two CW complexes with the source product-cell CW structure or proves the stated comparison with the ordinary product topology. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — quotient CW structure
For a CW pair (X,A), X/A inherits cells from X−A together with one new 0-cell, with attaching maps obtained by composing with the quotient map.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a CW pair (X,A), X/A inherits cells from X−A together with one new 0-cell, with attaching maps obtained by composing with the quotient map. Pinned/current Mathlib has quotient topology and CW subcomplex infrastructure, but no checked theorem constructs the claimed quotient CW structure on X/A with exactly the inherited non-A cells plus a new 0-cell. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — suspension and cone
The suspension SX is (X×I) with each end X×{0}, X×{1} collapsed to a point; the cone CX collapses X×{0} to one point.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The suspension SX is (X×I) with each end X×{0}, X×{1} collapsed to a point; the cone CX collapses X×{0} to one point. Pinned/current Mathlib has generic quotient and product topology machinery, but no checked topological suspension/cone construction owning this source unit. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — join
The join X*Y is (X×Y×I)/∼, collapsing the t=0 end along Y and the t=1 end along X.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The join X*Y is (X×Y×I)/∼, collapsing the t=0 end along Y and the t=1 end along X. Pinned/current Mathlib has generic quotient machinery, but no checked topological join construction with the stated two endpoint collapse relations. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — wedge sum
For based spaces, X∨Y is the disjoint union with the chosen basepoints identified; arbitrary wedges are formed analogously.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For based spaces, X∨Y is the disjoint union with the chosen basepoints identified; arbitrary wedges are formed analogously. Pinned/current Mathlib has coproduct/pushout infrastructure, but no checked based topological wedge construction owning the binary and arbitrary-wedge statement. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — smash product
For based spaces, X∧Y=(X×Y)/(X∨Y).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For based spaces, X∧Y=(X×Y)/(X∨Y). Pinned/current Mathlib has product/quotient infrastructure, but no checked based topological smash-product construction identifying the wedge subspace and quotient as stated. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.7
Graphs. The three graphs 0 → ∞ iff are homotopy equivalent since each is a deformation retract of a disk with two holes, but we can also deduce this from the collapsing criterion above since collapsing the middle edge of the first and third graphs produces the second graph.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Graphs. The three graphs 0 → ∞ iff are homotopy equivalent since each is a deformation retract of a disk with two holes, but we can also deduce this from the collapsing criterion above since collapsing the middle edge of the first and third graphs produces the second graph. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.8
Consider the space X obtained from S^{2} by attaching the two ends of an arc A to two distinct points on the sphere, say the north and south poles. Hence S^{2} / S^{0} and S^{1} ∨ S^{2} are homotopy equivalent, a fact which may not be entirely obvious at first glance.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Consider the space X obtained from S^{2} by attaching the two ends of an arc A to two distinct points on the sphere, say the north and south poles. Hence S^{2} / S^{0} and S^{1} ∨ S^{2} are homotopy equivalent, a fact which may not be entirely obvious at first glance. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.9
Let X be the union of a torus with n meridional disks. To obtain a CW structure on X, choose a longitudinal circle in the torus, intersecting each of the meridional disks in one point. Collapsing each meridional disk to a point yields a homotopy equivalent space Y consisting of n 2 spheres, each tangent to its two neighbors, a ‘necklace with n beads’.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let X be the union of a torus with n meridional disks. To obtain a CW structure on X, choose a longitudinal circle in the torus, intersecting each of the meridional disks in one point. Collapsing each meridional disk to a point yields a homotopy equivalent space Y consisting of n 2 spheres, each tangent to its two neighbors, a ‘necklace with n beads’. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — reduced suspension
For a based CW complex (X,x_0), the reduced suspension ΣX is obtained from SX by collapsing {x_0}×I; it is homotopy equivalent to SX.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a based CW complex (X,x_0), the reduced suspension ΣX is obtained from SX by collapsing {x_0}×I; it is homotopy equivalent to SX. The searches found no checked reduced-suspension object or theorem comparing it by homotopy equivalence to the unreduced suspension for based CW complexes. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.10
Reduced Suspension. Let X be a CW complex and x_{0} ∈ X a 0 cell. Inside the suspension S X we have the line segment { x_{0} } × I, and collapsing this to a point yields a space Σ X homotopy equivalent to S X, called the reduced suspension of X.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Reduced Suspension. Let X be a CW complex and x_{0} ∈ X a 0 cell. Inside the suspension S X we have the line segment { x_{0} } × I, and collapsing this to a point yields a space Σ X homotopy equivalent to S X, called the reduced suspension of X. The searches found no checked realization of Hatcher’s reduced-suspension example; generic quotient machinery alone does not own the construction-and-equivalence bundle. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Construction — attaching a space along a subspace
Given A⊂X_1 and f:A→X_0, the attachment X_0⊔_fX_1 is the quotient of X_0⊔X_1 identifying a with f(a).
Formalized. Mathlib/CategoryTheory/Limits/Types/Pushouts.lean::CategoryTheory.Limits.Types.Pushout, Types.Pushout.Rel, Types.Pushout.inl, Types.Pushout.inr; Mathlib/Topology/Category/TopCat/Limits/Basic.lean::TopCat.colimit_topology, TopCat.topCat_hasColimits — For the inclusion A → X₁ and map f : A → X₀, the TopCat pushout is the final-topology version of the type pushout, whose carrier is explicitly the quotient of X₁ ⊕ X₀ by the relation identifying the two images of each a. This is Hatcher’s attachment quotient.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction — mapping cone
For f:X→Y, C_f=Y⊔_fCX; equivalently C_f=M_f/X.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For f:X→Y, C_f=Y⊔_fCX; equivalently C_f=M_f/X. deancureton/sphere-six-complex supplies a mapping-cylinder construction, but neither it nor pinned/current Mathlib supplies the topological cone/mapping-cone construction and the stated identification C_f = M_f/X as a complete checked route. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.11
Let us rederive the result in Example 0.8 that a sphere with two points identified is homotopy equivalent to S^{1} ∨ S^{2}. Since A is contractible, this attaching map is homotopic to a constant map, and attaching S^{2} to S^{1} via a constant map of A yields S^{1} ∨ S^{2}.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let us rederive the result in Example 0.8 that a sphere with two points identified is homotopy equivalent to S^{1} ∨ S^{2}. Since A is contractible, this attaching map is homotopic to a constant map, and attaching S^{2} to S^{1} via a constant map of A yields S^{1} ∨ S^{2}. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.12
In similar fashion we can see that the necklace in Example 0.9 is homotopy equivalent to the wedge sum of a circle with n 2 spheres. The necklace can be obtained from a circle by attaching n 2 spheres along arcs, so the necklace is homotopy equivalent to the space obtained by attaching n 2 spheres to a circle at points. Then we can slide these attaching points around the circle until they all coincide, producing the wedge sum.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In similar fashion we can see that the necklace in Example 0.9 is homotopy equivalent to the wedge sum of a circle with n 2 spheres. The necklace can be obtained from a circle by attaching n 2 spheres along arcs, so the necklace is homotopy equivalent to the space obtained by attaching n 2 spheres to a circle at points. Then we can slide these attaching points around the circle until they all coincide, producing the wedge sum. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.13
Here is an application of the earlier fact that collapsing a contractible subcomplex is a homotopy equivalence: If (X, A) is a CW pair, consisting of a cell complex X and a subcomplex A, then X / A ≃ X ∪ C A, the mapping cone of the inclusion A ↪ X. For we have X / A = (X ∪ C A) / C A ≃ X ∪ C A since C A is a contractible subcomplex of X ∪ C A.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Here is an application of the earlier fact that collapsing a contractible subcomplex is a homotopy equivalence: If (X, A) is a CW pair, consisting of a cell complex X and a subcomplex A, then X / A ≃ X ∪ C A, the mapping cone of the inclusion A ↪ X. For we have X / A = (X ∪ C A) / C A ≃ X ∪ C A since C A is a contractible subcomplex of X ∪ C A. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Example 0.14
If (X, A) is a CW pair and A is contractible in X, that is, the inclusion A ↪ X is homotopic to a constant map, then X / A ≃ X ∨ S A. Namely, by the previous example we have X / A ≃ X ∪ C A, and then since A is contractible in X, the mapping cone X ∪ C A of the inclusion A ↪ X is homotopy equivalent to the mapping cone of a constant map, which is X ∨ S A.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If (X, A) is a CW pair and A is contractible in X, that is, the inclusion A ↪ X is homotopic to a constant map, then X / A ≃ X ∨ S A. Namely, by the previous example we have X / A ≃ X ∪ C A, and then since A is contractible in X, the mapping cone X ∪ C A of the inclusion A ↪ X is homotopy equivalent to the mapping cone of a constant map, which is X ∨ S A. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Definition — homotopy extension property
A pair (X,A) has the homotopy extension property if every compatible map on X×{0} and homotopy on A×I extends to X×I.
Formalized. deancureton/sphere-six-complex::SphereSixComplex/Topology/EstablishedStrongDeformationRetracts.lean::SphereSixComplex.HasHomotopyExtensionProperty; SphereSixComplex/Topology/CollarHomotopyExtension.lean::SphereSixComplex.HomotopyExtensionProperty — The pair form quantifies over target spaces, an initial map on X, and a homotopy on A, and returns a homotopy on X restricting to the prescribed one on A; this is exactly Hatcher’s HEP. The map-form interface is the equivalent inclusion formulation.
Searched: R=895c0a0661501581c34d42fea3c553d4f0ee43b1; Apache-2.0; Lean 4.34.0-rc1
Example 0.15
A pair (X, A) has the homotopy extension property if A has a mapping cylinder neighborhood in X, by which we mean a closed neighborhood N containing a subspace B, thought of as the boundary of N, with N - B an open neighborhood of A, such that there exists a map f {: } B {→ } A and a homeomorphism h {: } M_{f} {→ } N with h | A ∪ B = 1. Hence so does the homeomorphic pair (N, A ∪ B).
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A pair (X, A) has the homotopy extension property if A has a mapping cylinder neighborhood in X, by which we mean a closed neighborhood N containing a subspace B, thought of as the boundary of N, with N - B an open neighborhood of A, such that there exists a map f {: } B {→ } A and a homeomorphism h {: } M_{f} {→ } N with h | A ∪ B = 1. Hence so does the homeomorphic pair (N, A ∪ B). deancureton/sphere-six-complex::SphereSixComplex/Topology/MappingCylinderHomotopyExtension.lean::SphereSixComplex.mappingCylinderFree_homotopyExtensionProperty proves HEP for the free-end inclusion of a mapping cylinder, but does not prove Hatcher’s ambient mapping-cylinder-neighborhood criterion for (X,A). Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 0.16
If (X, A) is a CW pair, then X × {0 } ∪ A × I is a deformation retract of X × I, hence (X, A) has the homotopy extension property.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If (X, A) is a CW pair, then X × {0 } ∪ A × I is a deformation retract of X × I, hence (X, A) has the homotopy extension property. deancureton/sphere-six-complex::SphereSixComplex/Topology/RelativeCWHomotopyExtensionProof.lean::SphereSixComplex.hasHomotopyExtensionProperty_of_relativeCWComplex_proved, exists_skeletalRetraction, and exists_cellAttachmentRetraction prove the HEP consequence using a retraction of the L-shaped cylinder. The development explicitly requires only an ordinary retraction and does not prove the source row’s stronger assertion that X×{0} ∪ A×I is a deformation retract of X×I. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 0.17
If the pair (X, A) satisfies the homotopy extension property and 1 A is contractible, then the quotient map q {: } X {→ } X / A is a homotopy equivalence.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If the pair (X, A) satisfies the homotopy extension property and 1 A is contractible, then the quotient map q {: } X {→ } X / A is a homotopy equivalence. The audited HEP developments prove HEP-to-strong-deformation-retract results under a homotopy-equivalence hypothesis, but no checked theorem gives the quotient-collapse homotopy equivalence from HEP plus contractibility of A. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 0.18
If (X_{1}, A) is a CW pair and we have attaching maps f, g: A → X_{0} that are homotopic, then X_{0} ⊔{f} X{1} ≃ X_{0} ⊔{g} X{1} rel X_{0}.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If (X_{1}, A) is a CW pair and we have attaching maps f, g: A → X_{0} that are homotopic, then X_{0} ⊔{f} X{1} ≃ X_{0} ⊔{g} X{1} rel X_{0}. Topological pushouts and relative homotopy are available, but no checked declaration proves that homotopic attaching maps yield homotopy-equivalent attached spaces rel X₀ under the stated CW-pair hypothesis. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Proposition 0.19
Suppose (X, A) and (Y, A) satisfy the homotopy extension property, and f: X {→ } Y is a homotopy equivalence with f | A = 1.. Then f is a homotopy equivalence rel A.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Suppose (X, A) and (Y, A) satisfy the homotopy extension property, and f: X {→ } Y is a homotopy equivalence with f | A = 1.. Then f is a homotopy equivalence rel A. deancureton/sphere-six-complex::SphereSixComplex/Topology/RelativeHomotopy.lean::SphereSixComplex.HomotopyExtensionProperty.exists_strongDeformationRetractData proves the acyclic-cofibration strong-deformation-retract theorem for one map. No checked declaration packages the full two-pair relative homotopy-equivalence theorem for a map fixing A. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.
Corollary 0.20
If (X, A) satisfies the homotopy extension property and the inclusion A ↪ X is a homotopy equivalence, then A is a deformation retract of X.
Formalized. deancureton/sphere-six-complex::SphereSixComplex/Topology/EstablishedStrongDeformationRetracts.lean::SphereSixComplex.strongDeformationRetraction_of_cofibration_homotopyEquivalence, HomotopyExtensionProperty.nonempty_strongDeformationRetraction — The first theorem assumes the pair HEP and that the subspace inclusion is a homotopy equivalence and returns a strong deformation retraction onto the subspace. It is exactly Hatcher Corollary 0.20, in fact with the stronger stationary homotopy conclusion.
Searched: R=895c0a0661501581c34d42fea3c553d4f0ee43b1; Apache-2.0; Lean 4.34.0-rc1
Corollary 0.21
A map f: X {→ } Y is a homotopy equivalence iff X is a deformation retract of the mapping cylinder M_{f}. Hence, two spaces X and Y are homotopy equivalent iff there is a third space containing both X and Y as deformation retracts.
Not formalized. none; no complete checked declaration under strict bundle semantics — As of 2026-09-06, no checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A map f: X {→ } Y is a homotopy equivalence iff X is a deformation retract of the mapping cylinder M_{f}. Hence, two spaces X and Y are homotopy equivalent iff there is a third space containing both X and Y as deformation retracts. deancureton/sphere-six-complex has TopCat.MappingCylinder, mappingCylinderBaseHomotopyEquiv, mappingCylinderFree_homotopyExtensionProperty, mappingCylinderFree_isHomotopyEquivalence, and HEP+homotopy-equivalence ⇒ strong-deformation-retract data. These ingredients cover substantial directions, but no checked declaration owns the full iff plus the second common-ambient-space characterization required by this bundled row. Strict bundle semantics reject a specialization, a semantically adjacent construction, one clause/example of a bundled row, or a proper subset as the route for this ID.