Simplicial and singular homology
Hatcher §2.1 (pages 102–133). The completed first slice covers singular homology, its low-degree checks, functoriality, and homotopy invariance through Corollary 2.11 and Proposition 2.12. A second selected slice decomposes reduced and relative homology, exact sequences, naturality, and relative homotopy invariance; all fifteen of its leaves are complete. A third four-leaf slice covers the long exact sequence of a triple and its naturality; all four leaves are complete. A fourth ten-leaf slice decomposes small chains and excision; all ten leaves are complete. A fifth fifteen-leaf slice covers the good-pair quotient comparison, quotient exact sequence, and naturality; all fifteen leaves are formalized locally and complete. A sixth selected slice formalizes the post-excision applications through Theorem 2.26 in twenty-seven leaves, with five supporting Appendix A.5 leaves; all thirty-two are complete. The separately placed sphere branch is complete through the three-leaf Corollary 2.15 milestone.
Simplicial homology takes a Δ-complex structure and forms the chain complex of
its simplices; it is finite and computable but depends on the chosen structure.
Singular homology takes all continuous maps Δⁿ → X as generators; it is
manifestly functorial but visibly enormous. The section
proves homotopy invariance of singular homology by a prism decomposition,
builds the long exact sequence of a pair, proves excision by barycentric
subdivision, and concludes that the two theories agree on Δ-complexes.
The pinned Mathlib has exact categorical versions of most of the first slice.
The roadmap makes those upstream results explicit, and the two thin
source-facing consequences are formalized locally in
Hatcher/Singular/Homology.lean. It also contains the generic algebraic long
exact sequence and, at the current v4.34.1 pin, the SSetPair relative-
homology foundation from PR #41285. The four reduced-homology leaves, generic
algebraic exact-sequence leaf, simplicial-pair foundation, singular-pair
functor, relative-homology functor, pair long exact sequence, and pair-sequence
naturality are complete. The pair sequence includes the integral connecting-map
formula, and the relative homotopy branch through Proposition 2.19, the reduced
pair sequence with its naturality, and the pointed comparison are complete. The
topological-triple interface, chain-level short exact sequence, induced long
exact sequence with its degree-zero endpoint, and naturality are also complete.
Singular chains and low degrees
For a coefficient object R in a preadditive category with coproducts and a
topological space X, form the chain complex freely generated in degree n
by continuous maps from the standard n-simplex to X, with differential the
alternating sum of face restrictions.
The pinned definition
AlgebraicTopology.singularChainComplexFunctor packages this construction as
a functor in both the coefficient object and the space. Its implementation is
the chain complex of the singular simplicial set TopCat.toSSet.obj X.
Dependencies
For a coefficient object R, a space X, and n : ℕ, define Hₙ(X; R) as
the degree-n homology object of the singular chain complex of X.
The pinned definition AlgebraicTopology.singularHomologyFunctor is functorial
in R and X. Hatcher's group Hₙ(X) is its specialization to abelian groups
with coefficient object ℤ.
Dependencies
Hatcher, Proposition 2.7 (pages 109–110). For a space X, zeroth
singular homology with coefficients in R is isomorphic to the
coproduct of one copy of R for each path component of X. In particular, a
nonempty path-connected space has integral zeroth homology isomorphic to ℤ.
The pinned definition TopCat.singularHomology₀Iso gives the component-indexed
isomorphism using ZerothHomotopy X. The associated augmentation is
TopCat.singularHomology₀ε, and Mathlib supplies its IsIso instance for a
path-connected space.
Sources
Dependencies
For a totally disconnected space X and n ≠ 0, the degree-n singular
homology object of X is zero. This pinned theorem is stronger than the
positive-degree clause of Hatcher's point calculation and supplies that clause
after specializing X to a one-point space.
Sources
Dependencies
Hatcher, Proposition 2.8 (page 110). Fix the one-point model
TopCat.of PUnit. Its degree-zero singular homology is isomorphic to the
coefficient object R, and its degree-n homology is zero for every n ≠ 0.
The theorem Hatcher.Singular.point_homology packages both clauses. Its
supporting declarations are pointHomologyZeroIso, obtained from the
degree-zero augmentation, and isZero_pointHomology, a thin specialization of
Mathlib's theorem for totally disconnected spaces. For Hatcher's statement,
specialize the coefficient category to AddCommGrpCat and R to
AddCommGrpCat.of ℤ.
Formalized in Hatcher/Singular/Homology.lean.
Sources
Dependencies
Functoriality and homotopy invariance
Hatcher, Proposition 2.9 (page 111). A chain map between chain complexes induces a morphism between their homology objects in every degree.
The pinned definition HomologicalComplex.homologyMap is the categorical
construction. Its companion lemmas homologyMap_id and homologyMap_comp
give the identity and composition laws used in Corollary 2.11.
Sources
Dependencies
Hatcher, Proposition 2.12 (page 113). If two chain maps are chain homotopic, their induced morphisms on homology are equal in every degree.
This is exactly the pinned lemma Homotopy.homologyMap_eq.
Sources
Dependencies
For homotopic maps f,g : X ⟶ Y, the induced maps between singular chain
complexes are chain homotopic.
The pinned definition
TopCat.Homotopy.singularChainComplexFunctorObjMap constructs this homotopy
through the singular simplicial set. It fills the same role as Hatcher's prism
operator, but it is not a formalization of Hatcher's explicit prism formula.
Hatcher, Theorem 2.10 (pages 111–113). If continuous maps f,g : X → Y
are homotopic, their induced maps on singular homology are equal in every
degree. The exact pinned statement is
homologyMap (((singularChainComplexFunctor C).obj R).map f) n =
homologyMap (((singularChainComplexFunctor C).obj R).map g) n.
This is exactly the pinned lemma
TopCat.Homotopy.congr_homologyMap_singularChainComplexFunctor.
Sources
Hatcher, Corollary 2.11 (page 111). For topological spaces X and Y, a
homotopy equivalence e : X ≃ₕ Y, a coefficient object R : C, and a degree
n, define an isomorphism between their degree-n singular homology objects.
Here C has a category structure, coproducts, a preadditive structure, and
homology.
The noncomputable definition is
Hatcher.Singular.homologyIsoOfHomotopyEquiv. Its source is
ContinuousMap.HomotopyEquiv; its target is an Iso from
((singularHomologyFunctor C n).obj R).obj (TopCat.of X) to the corresponding
object for Y; and its forward morphism is induced by e.toFun.
Construct the inverse from e.invFun, then use functoriality and homotopy
invariance for the two inverse laws. Mathlib's generic
HomotopyEquiv.toHomologyIso is additional chain-complex-level prior art, but
there is no pinned topological theorem with this interface.
Formalized in Hatcher/Singular/Homology.lean.
Sources
Dependencies
Reduced and relative homology
Small chains, good-pair quotients, and post-excision applications
Small chains and excision, covering Proposition 2.21 and Theorem 2.20, are decomposed into ten formalizable leaves, all formalized locally.
Good pairs and quotient exact sequences decompose Proposition 2.22, Theorem 2.13, their canonical point-quotient maps, and naturality into fifteen formalizable leaves, all formalized locally and complete.
Post-excision applications formalize the arbitrary-pair mapping-cone comparison, Example 2.23, Corollaries 2.24–2.25, and Theorem 2.26. The complete branch is placed after the sphere calculation in dependency order while retaining its §2.1 source binding.
Lemma 2.1 and Examples 2.2–2.5 need a source-faithful Δ-complex chain model.
Proposition 2.6 needs additivity over all path components in every degree;
Mathlib v4.34.1 contains only its degree-zero case. Example 2.17, the
remaining Δ-complex work, and Theorem 2.27 remain deferred. Corollary 2.15 is complete in
the sphere-homology and Brouwer
milestone.
Relative homology for simplicial-set pairs merged in Mathlib PR
#41285 and is
present at the repository's v4.34.1 pin. The simplicial-pair foundation is
therefore complete, and
the singular-pair functor and
relative singular homology
are now formalized. The
pair long exact sequence,
including its connecting-map formula, is also formalized. Pair-sequence
naturality is now formalized. The compatible relative chain homotopy and its
induced homology-map equality complete the relative homotopy branch and
Proposition 2.19. The reduced pair sequence, its naturality, and the pointed
comparison are now formalized. All four local triple-sequence leaves are now
formalized. The excision target is now decomposed locally; Riou's independent
implementation remains active upstream prior art. The completed good-pair
milestone uses a functorial TopCat pushout model for X/A; no exact endpoint is
present in pinned Mathlib.