Appendix. Topology of Cell Complexes
FC07 — Hatcher, Algebraic Topology.
This chapter contains 9 definitions, 2 theorems, 13 propositions, 4 corollaries and 4 constructions.
Of the 32 statements checked against Lean, 10 are formalized somewhere and 22 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 22 | 69% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 10 | 31% | Mathlib states and proves it. |
| checked in total | 32 |
- Canonical source block: FC07 Hatcher Appendix,
FC07-CA-U001–FC07-CA-U032, exactly 32 unique contiguous rows retrieved from FC07 — Hatcher, Algebraic Topology throughagent-memory. - Search order followed the established FC07 contract: project source first at
A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean 4.33.0), current upstream MathlibH=80cbd0498ab39e21d24d6730b3f932cec672a702(Apache-2.0, Lean 4.34.0-rc2), current/open and indexed search, Reservoir/packages, broad discoverable Lean repositories, and local reference mirrors. Noproject-existing,package-import, or admissiblereference-portowner was found. - Every promoted Mathlib path exists at exact P and every promoted declaration was compiled through the project toolchain. Two nontrivial exact consequences were also compiled as local audit witnesses: U001’s skeletonwise weak-topology iff from
CWComplex.closed, and U023’s product-of-a-quotient-map theorem fromIsQuotientMap.continuous_lift_prod_left. Audit witnesses are evidence only, not project source. - CA has 10 pinned positive rows and 22 dated unmatched rows. The positives are U001 (weak topology), U003 (characteristic-map CW criterion packaged as
CWComplex), U018 (compact-open topology), U019 (compact-domain sup metric), U020 (evaluation/exponential-law continuity), U023 (quotient map × locally compact identity), U027 (simplicial set), U028 (singular complex), U030 (degenerate simplex), and U031 (geometric realization). - U002 is deliberately not promoted from
facebookresearch/atlas-lean::Atlas/AlgebraicTopologyI/code/Section15.lean::CWSubcomplex.compact_subset_finite_subcomplex: the declaration’s proof isby sorry. U011 likewise is not routed through Atlas’sIsNeighborhoodRetract: that declaration covers an already embedded Euclidean subset rather than Hatcher’s arbitrary-space existence-of-embedding predicate, and the repository license is CC BY-NC 4.0 with an additional no-training rider, so it is not treated as a portable source route. - U024 remains unmatched after checking the Apache-2.0 LeanPool HEP development at
Vilin97/lean-poolrevision3fc79f0a795f19fffcc59eee3efaf5faa52de3c3: it definesHasHomotopyExtensionProperty/IsCofibrationand nearby retractions, but no checked iff identifies HEP with a retraction ofX × IontoX × {0} ∪ A × I. - U022 is not inferred from
Homeomorph.curry: the pinned homeomorphism has stronger local-compactness assumptions than Hatcher’s exact Y-locally-compact, Z-Hausdorff theorem. U021 is not inferred from generic compactly-generated machinery without the stated product theorem. - U031 is an equivalent categorical realization, not a name-only match:
SSet.toTopis explicitly the geometric-realization functor, constructed as the left Kan extension of standard topological simplices along Yoneda, andtoTopSimplexidentifies representables with the corresponding topological simplices. This is the colimit presentation equivalent to the quotient by all simplex-structure identifications. - U032 is deliberately not promoted. P and H have degreewise categorical products of simplicial sets, and current
TopAdj.leanequips the right adjointTopCat.toSSetwith monoidal/product structure, but no checked declaration proves that geometric realizationSSet.toToppreserves products. A TauCeti Lean source encountered in broad discovery explicitly leaves identifying realization with products for later work. - Current upstream was refreshed on 2026-09-07;
H=80cbd0498ab39e21d24d6730b3f932cec672a702remained the newest Mathlib HEAD observed and uses Lean 4.34.0-rc2. No new H endpoint closed the unmatched ENR/CW-local-contractibility/product-realization rows. - This Appendix is the final canonical FC07 block: the catalogue contains no units after
FC07-CA-U032. With CA promoted, FC07 Sweep II is complete. N=2026-09-07denotes a dated unmatched result after the prescribed search layers. Strict whole-row semantics are uniform: a proper subset of a multi-clause row, a hypothesis-mismatched theorem, an unproved declaration, or a licensing-incompatible external source is not credited as a route.
Definition/convention — weak topology for CW complexes
A CW complex X=⋃_nX^n has the weak topology: A⊂X is open (equivalently closed) iff A∩X^n is open (respectively closed) in each skeleton.
Formalized. Mathlib/Topology/CWComplex/Classical/Basic.lean::Topology.CWComplex.closed, Topology.RelCWComplex.skeleton, Topology.RelCWComplex.closedCell_subset_skeleton, Topology.RelCWComplex.isClosed_closedCell — CWComplex.closed is Mathlib’s cellwise weak-topology criterion. Together with the skeleton containment and closed-cell lemmas, it proves the equivalent Hatcher criterion that a subset is closed iff its intersection with every skeleton is relatively closed; that exact equivalence was compiled as an audit witness at P.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition A.1
A compact subspace of a CW complex is contained in a finite subcomplex.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A compact subspace of a CW complex is contained in a finite subcomplex. Atlas contains CWSubcomplex.compact_subset_finite_subcomplex, but its body is by sorry; current Mathlib has only finite-indexed-subcomplex finiteness, not the compact-subset theorem. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Proposition A.2
Let X be Hausdorff and Φ_α:D_α^n→X a family of maps. They are characteristic maps of a CW structure iff: (i) each Φ_α maps int D_α^n homeomorphically onto a cell, these cells are disjoint, and they cover X; (ii) each boundary image lies in a finite union of lower-dimensional cells; (iii) C⊂X is closed iff C meets the closure of every cell in a closed set.
Formalized. Mathlib/Topology/CWComplex/Classical/Basic.lean::Topology.CWComplex, Topology.CWComplex.pairwiseDisjoint, Topology.CWComplex.mapsTo, Topology.CWComplex.closed, Topology.CWComplex.union — CWComplex is precisely the characteristic-map presentation used in Proposition A.2: disk interiors map homeomorphically to pairwise-disjoint cells covering the complex, boundaries land in finitely many lower-dimensional cells, and CWComplex.closed is the weak-topology closure criterion. This is the proposition’s data/axioms packaged as a structure rather than a separate iff theorem.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition A.3
CW complexes are normal, and in particular, Hausdorff.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: CW complexes are normal, and in particular, Hausdorff. Pinned/current CW APIs assume Hausdorffness for many closed-cell lemmas; no checked theorem derives normality or Hausdorffness for every CW complex. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Proposition A.4
Each point in a CW complex has arbitrarily small contractible open neighborhoods, so CW complexes are locally contractible.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Each point in a CW complex has arbitrarily small contractible open neighborhoods, so CW complexes are locally contractible. No checked theorem gives arbitrarily small contractible open neighborhoods or local contractibility for arbitrary CW complexes. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Proposition A.5
For a subcomplex A of a CW complex X, the open neighborhood N_{ε} (A) deformation retracts onto A if ε_{α} < 1 for all α.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a subcomplex A of a CW complex X, the open neighborhood N_{ε} (A) deformation retracts onto A if ε_{α} < 1 for all α. Subcomplex and homotopy machinery exists, but no checked construction of Hatcher’s N_ε(A) and its deformation retraction was found. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Definition — topology generated by subspaces
A space X is generated by subspaces X_α when X=⋃X_α and A⊂X is closed iff every A∩X_α is closed in X_α.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A space X is generated by subspaces X_α when X=⋃X_α and A⊂X is closed iff every A∩X_α is closed in X_α. TopologicalSpace.coinduced/generatedBy provide generic final-topology machinery, but no checked named interface realizes the full specified-family-of-subspaces closure criterion. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Construction — compactly generated topology
For a space X, X_c is the topology generated by its compact subspaces; X and X_c have the same compact subsets, and locally compact spaces satisfy X=X_c.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a space X, X_c is the topology generated by its compact subspaces; X and X_c have the same compact subsets, and locally compact spaces satisfy X=X_c. TopologicalSpace.compactlyGenerated and CompactlyGeneratedSpace formalize k-generation by compact Hausdorff probes, but no checked bundle proves Hatcher’s stated same-compact-subsets clause together with local-compact equality for X_c. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Theorem A.6
For CW complexes X and Y with characteristic maps Φ_{α} and Psi_{β}, the product maps Φ_{α} × Psi_{β} are the characteristic maps for a CW complex structure on (X × Y){c}. If either X or Y is compact or more generally locally compact, then (X × Y){c} = X × Y. Also, (X × Y)_{c} = X × Y if both X and Y have countably many cells.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For CW complexes X and Y with characteristic maps Φ_{α} and Psi_{β}, the product maps Φ_{α} × Psi_{β} are the characteristic maps for a CW complex structure on (X × Y){c}. If either X or Y is compact or more generally locally compact, then (X × Y){c} = X × Y. Also, (X × Y)_{c} = X × Y if both X and Y have countably many cells. No checked product-CW theorem supplies Hatcher’s characteristic product cells together with the compactly-generated/product-topology coincidence clauses. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Theorem A.7
A compact subspace K of ℝ^{n} is a retract of some neighborhood iff K is locally contractible in the weak sense that for each x ∈ K and each neighborhood U of x in K there exists a neighborhood V ⊂ U of x such that the inclusion V ↪ U is nullhomotopic.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A compact subspace K of ℝ^{n} is a retract of some neighborhood iff K is locally contractible in the weak sense that for each x ∈ K and each neighborhood U of x in K there exists a neighborhood V ⊂ U of x such that the inclusion V ↪ U is nullhomotopic. No checked Lean theorem gives the compact-subset-of-Euclidean-space neighborhood-retract iff weak-local-contractibility criterion. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Definition — Euclidean neighborhood retract
X is an ENR if it embeds in some ℝ^n as a retract of a neighborhood of its image.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: X is an ENR if it embeds in some ℝ^n as a retract of a neighborhood of its image. Atlas defines IsNeighborhoodRetract for an already embedded Euclidean subset, but it does not package Hatcher’s arbitrary-space embedding definition and its CC BY-NC/no-training license is not a portable project route. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Corollary A.8
A compact space is an ENR iff it can be embedded as a retract of a finite simplicial complex. Hence the homology groups and the fundamental group of a compact ENR are finitely generated.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A compact space is an ENR iff it can be embedded as a retract of a finite simplicial complex. Hence the homology groups and the fundamental group of a compact ENR are finitely generated. No checked theorem proves the stated ENR characterization/application. Atlas mentions nearby ENR facts but the relevant theorem bodies are sorry-backed or do not own this row. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Corollary A.9
Every compact manifold, with or without boundary, is an ENR.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every compact manifold, with or without boundary, is an ENR. No checked theorem proves the stated ENR characterization/application. Atlas mentions nearby ENR facts but the relevant theorem bodies are sorry-backed or do not own this row. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Corollary A.10
Every finite CW complex is an ENR.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every finite CW complex is an ENR. No checked theorem proves the stated ENR characterization/application. Atlas mentions nearby ENR facts but the relevant theorem bodies are sorry-backed or do not own this row. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Definition — domination
Y is dominated by X if there are maps Y→iX→rY with ri≃id_Y.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Y is dominated by X if there are maps Y→iX→rY with ri≃id_Y. Homotopy and homotopy equivalence are formalized, but no checked dominated predicate packages maps Y→X→Y with composite homotopic to id. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Proposition A.11
A space dominated by a CW complex is homotopy equivalent to a CW complex.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A space dominated by a CW complex is homotopy equivalent to a CW complex. No checked domination-to-CW or compact-manifold-to-CW homotopy-equivalence theorem was found. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Corollary A.12
A compact manifold is homotopy equivalent to a CW complex.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A compact manifold is homotopy equivalent to a CW complex. No checked domination-to-CW or compact-manifold-to-CW homotopy-equivalence theorem was found. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Definition — compact-open topology
On the mapping space X^Y, the compact-open topology has subbasis M(K,U)={f:f(K)⊂U} for compact K⊂Y and open U⊂X.
Formalized. Mathlib/Topology/CompactOpen.lean::ContinuousMap.compactOpen, ContinuousMap.compactOpen_eq, ContinuousMap.isOpen_setOfPred_mapsTo — ContinuousMap.compactOpen is generated by the subbasic sets of continuous maps carrying a compact K into an open U; compactOpen_eq and isOpen_setOfPred_mapsTo expose exactly Hatcher’s M(K,U) definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition A.13
If X is a metric space and Y is compact, then the compact-open topology on X^{Y} is the same as the metric topology defined by the metric d (f, g) = {s u p }_{y ∈ Y} d (f (y), g (y)).
Formalized. Mathlib/Topology/UniformSpace/CompactConvergence.lean::ContinuousMap.compactConvergenceUniformSpace, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn; Mathlib/Topology/ContinuousMap/Compact.lean::ContinuousMap.instMetricSpace, ContinuousMap.dist_eq_iSup — Pinned Mathlib identifies compact convergence on continuous maps with the compact-open topology; for compact domain and metric codomain the induced metric on C(Y,X) satisfies dist f g = ⨆ y, dist (f y) (g y). Thus the compact-open topology is exactly Hatcher’s sup-metric topology.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition A.14
For the compact-open topology: (a) evaluation e:X^Y×Y→X, e(f,y)=f(y), is continuous when Y is locally compact; (b) if f:Y×Z→X is continuous then its adjoint hat(f):Z→X^Y is continuous; (c) the converse to (b) holds when Y is locally compact.
Formalized. Mathlib/Topology/CompactOpen.lean::ContinuousEval, continuous_eval, ContinuousMap.curry, ContinuousMap.continuous_of_continuous_uncurry, ContinuousMap.continuous_uncurry_of_continuous — ContinuousEval/continuous_eval give joint evaluation continuity under the locally-compact-pair hypothesis (hence for locally compact Y). continuous_of_continuous_uncurry gives the adjoint direction without local compactness, while continuous_uncurry_of_continuous gives the converse when Y is locally compact. These are exactly parts (a)–(c), up to product-coordinate order.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition A.15
If X is a compactly generated Hausdorff space and Y is locally compact, then the product topology on X × Y is compactly generated.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X is a compactly generated Hausdorff space and Y is locally compact, then the product topology on X × Y is compactly generated. CompactlyGeneratedSpace and locally compact instances exist, but no checked theorem proves the product of a compactly generated Hausdorff space with an arbitrary locally compact space is compactly generated. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Proposition A.16
The map X^{Y × Z} {→ } (X{Y}){Z}, f ↦ {hat(f) }, is a homeomorphism if Y is locally compact Hausdorff and Z is Hausdorff.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The map X^{Y × Z} {→ } (X{Y}){Z}, f ↦ {hat(f) }, is a homeomorphism if Y is locally compact Hausdorff and Z is Hausdorff. Homeomorph.curry gives an exponential-law homeomorphism only under stronger local-compactness hypotheses on both factors; no checked theorem matches Hatcher’s Y-locally-compact, Z-Hausdorff hypothesis bundle. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Proposition A.17
If f: X {→ } Y is a quotient map then so is f × 1: X × Z → Y × Z whenever Z is locally compact.
Formalized. Mathlib/Topology/CompactOpen.lean::Topology.IsQuotientMap.continuous_lift_prod_left; Mathlib/Topology/Maps/Basic.lean::isQuotientMap_iff; Mathlib/Topology/Order.lean::isOpen_iff_continuous_mem — continuous_lift_prod_left is the locally-compact product lifting property for a quotient map. Combining it with the Sierpiński-space characterization of open sets and the quotient-map criterion gives exactly that f × id_Z is quotient for locally compact Z; the complete theorem was compiled as an audit witness at P.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition A.18
A pair (X, A) has the homotopy extension property if and only if X × {0 } ∪ A × I is a retract of X × I.
Not formalized. none; no complete checked declaration under strict bundle semantics — 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 and only if X × {0 } ∪ A × I is a retract of X × I. LeanPool formalizes topological HEP/cofibration predicates, but no checked theorem proves HEP iff X×{0}∪A×I is a retract of X×I. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Definition — regular CW complex and simplicial complex
A CW complex is regular if characteristic maps can be chosen embeddings. A simplicial complex is a regular unordered Δ-complex in which each simplex is uniquely determined by its vertices.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A CW complex is regular if characteristic maps can be chosen embeddings. A simplicial complex is a regular unordered Δ-complex in which each simplex is uniquely determined by its vertices. Simplicial complexes and CW complexes exist separately, but no checked regular-CW predicate plus Hatcher’s unique-vertex-determined characterization owns the entire row. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Definition/construction — singular Δ-complex
A singular Δ-complex (sΔ-complex) broadens a Δ-complex by allowing simplices to be attached along arbitrary simplicial maps, hence supports quotient and attachment constructions.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A singular Δ-complex (sΔ-complex) broadens a Δ-complex by allowing simplices to be attached along arbitrary simplicial maps, hence supports quotient and attachment constructions. No checked singular-Δ-complex interface allowing arbitrary simplicial attaching maps was found. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Definition — simplicial set
Let Δ_* be the category of finite ordered simplices with order-preserving maps. A simplicial set is a contravariant functor Δ_*→Sets.
Formalized. Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean::SSet — SSet abbreviates simplicial objects in Type, i.e. functors SimplexCategoryᵒᵖ ⥤ Type, exactly contravariant functors from finite ordered simplices to sets.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — singular complex
For a space X, the singular complex S(X) is the simplicial set whose n-simplices are all continuous maps Δ^n→X, with structure maps by precomposition.
Formalized. Mathlib/AlgebraicTopology/SingularSet.lean::TopCat.toSSet, TopCat.toSSetObjEquiv — TopCat.toSSet is the singular simplicial set. toSSetObjEquiv identifies its n-simplices with continuous maps from the standard topological n-simplex to X, and functoriality is precomposition by simplex maps.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition A.19
Every simplicial set is isomorphic to one of the form Δ (X) for some s complex X which is unique up to isomorphism.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every simplicial set is isomorphic to one of the form Δ (X) for some s complex X which is unique up to isomorphism. Pinned Mathlib realizes simplicial sets as presheaves and has geometric realization, but no checked sΔ-complex reconstruction/uniqueness theorem realizes Proposition A.19. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.
Definition — degenerate simplex
An n-simplex of a simplicial set is degenerate if it lies in the image of a structure map induced by a noninjective (equivalently surjective after factorization) simplex map.
Formalized. Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean::SSet.degenerate, SSet.mem_degenerate_iff, SSet.degenerate_eq_iUnion_range_σ — SSet.degenerate defines an n-simplex to lie in the range of a structure map to lower dimension; mem_degenerate_iff factors through an epi/surjective simplex map, and degenerate_eq_iUnion_range_σ gives the usual degeneracy-map formulation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — geometric realization
For a simplicial set Y, its geometric realization |Y| is the quotient obtained from simplices Y_n×Δ^n by the standard identifications induced by morphisms in Δ_*.
Formalized. Mathlib/AlgebraicTopology/SingularSet.lean::SSet.toTop, SSet.toTopSimplex, sSetTopAdj — SSet.toTop is explicitly Mathlib’s geometric-realization functor, defined as the left Kan extension of the standard topological simplex along Yoneda; toTopSimplex identifies representables with standard simplices. This is the categorical colimit form of Hatcher’s quotient of all Y_n × Δ^n by the structure-map identifications.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — product of simplicial sets
The product simplicial set has (X×Y)_n=X_n×Y_n with structure maps acting componentwise, and geometric realization preserves this product (with the compactly generated CW topology).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The product simplicial set has (X×Y)_n=X_n×Y_n with structure maps acting componentwise, and geometric realization preserves this product (with the compactly generated CW topology). Degreewise products of simplicial sets are available categorically, but neither P nor current H proves that SSet.toTop preserves products; current TopAdj equips the right adjoint TopCat.toSSet, not realization, with monoidal/product structure. Strict bundle semantics reject specializations, stronger/weaker hypothesis substitutions, adjacent constructions, isolated clauses/examples, sorry-backed results, and nonportable source-only near-matches.