Relative homology and exact sequences
Hatcher §2.1 (pages 110, 113–124, and 127–128). The selected slices introduce reduced homology from the augmented singular complex, relative homology of a topological pair, pair and triple long exact sequences, homotopy invariance, and naturality. A fourth milestone continues through small chains and excision and is decomposed into ten formalizable leaves, all complete. A fifth, fifteen-leaf milestone covers good pairs, Proposition 2.22, Theorem 2.13, and the quotient sequence's naturality; all fifteen leaves are formalized locally and complete.
The mathematical source is Hatcher. The representation against Mathlib is
fixed separately in the
project-authored implementation specification.
The four-node reduced-homology branch and the generic algebraic exact-sequence
node are complete. The SSetPair relative-homology foundation is also complete
because the current Mathlib v4.34.1 pin contains PR #41285, and
the singular-pair functor is formalized locally.
Relative singular homology is also
formalized, as is the pair long exact sequence,
including its connecting-map formula and naturality. The compatible relative
chain homotopy and induced homology-map equality complete the relative homotopy
branch and Proposition 2.19. The reduced pair sequence, its naturality, and the
pointed comparison are also formalized. Thus all fifteen leaves in the
reduced- and relative-pair slice are complete. All four leaves in the
triple-sequence slice are formalized locally as well.
Reduced homology
Hatcher, §2.1 (page 110). For a space X and coefficient object R,
augment the singular chain complex by the map from degree-zero chains to R
that sends every singular zero-simplex to the identity of R.
The main artifact should be
Hatcher.Reduced.augmentedSingularChainComplexFunctor. Mathlib's
ChainComplex.augment shifts the ordinary singular complex up one degree, so
degree zero is R and degree n + 1 is Cₙ(X;R). Supporting declarations
construct the natural chain-level augmentation and prove that the degree-one
boundary followed by it is zero.
The construction is coefficient-general in an abelian category with the
required coproducts. Hatcher's complex is its integral specialization. The
functor may be defined for the empty space as well; the roadmap's
nonnegative-degree groups then extend Hatcher's convention, which suppresses
the degree -1 group by working with nonempty spaces.
Dependencies
Hatcher, §2.1 (pages 110 and 113). Define reduced singular homology
Ḥₙ(X;R) as degree n + 1 homology of the augmented singular chain
complex. Continuous maps induce maps on these groups, giving a functor in the
space.
The main artifact should be Hatcher.Reduced.homologyFunctor. It must use the
augmented complex rather than define reduced homology through a chosen
basepoint; the latter is a theorem in Example 2.18. Defining the functor on the
empty space is harmless in the displayed nonnegative degrees and is recorded
as an extension of Hatcher's nonempty-space convention.
Sources
Dependencies
Hatcher, §2.1 (page 110). For every space X, coefficient object R,
and positive degree n, construct the natural isomorphism
Ḥₙ(X;R) ≅ Hₙ(X;R).
The main artifact should be Hatcher.Reduced.homologyIsoOfPositiveDegree.
It is induced by the degree shift in ChainComplex.augment, not by choosing a
basepoint.
Hatcher, §2.1 (page 110). For a space X with a chosen point and
coefficient object R, split the augmentation to obtain
H₀(X;R) ≅ H̃₀(X;R) ⊞ R.
The main artifact should be Hatcher.Reduced.homologyZeroIso. The chosen
point supplies a section of the augmentation. The result is deliberately not
claimed to be natural for unpointed spaces.
Relative chains and homology
For a monomorphism A ⟶ X of simplicial sets, form the cokernel chain
complex Cₙ(X;R) / Cₙ(A;R), its homology functor, the quotient map from
absolute chains, and the connecting morphisms and exactness results relating
the homology of A, X, and (X,A).
At the current Mathlib v4.34.1 pin, the main artifact is the upstream
definition SSetPair.homologyFunctor in
Mathlib/AlgebraicTopology/SimplicialSet/Homology/Relative.lean; its supporting
API includes SSetPair.chainComplex, homologyπ, homologyδ, and
homology_exact₁/₂/₃.
Mathlib v4.34.1 contains PR #41285, so this foundational node is complete.
The singular-pair functor is now formalized, and
relative singular homology is formalized on
top of it.
Dependencies
For a topological pair P, apply TopCat.toSSet to the embedding
P.map : P.snd ⟶ P.fst and prove the resulting simplicial map is a
monomorphism. This defines a functor from topological pairs to simplicial-set
pairs while preserving maps of pairs.
Formalized as
Hatcher.Relative.singularPairFunctor : TopPair ⥤ SSetPair in
Hatcher/Singular/Relative.lean. The direction respects the two APIs:
TopPair.fst is the ambient space and
SSetPair.right is the ambient simplicial set. Joël Riou's excision prototype
contains a compatible TopPair.toSSetPair, but it is implementation prior art,
not a pinned dependency.
Sources
Dependencies
Hatcher, §2.1 (pages 115–118). For a topological pair (X,A), define
relative singular chains as Cₙ(X;R) / Cₙ(A;R) and relative singular
homology as their homology. A map of pairs induces the corresponding map on
relative chains and homology.
Formalized as Hatcher.Relative.homologyFunctor, with
Hatcher.Relative.chainComplexFunctor for relative chains and
Hatcher.Relative.chainComplexFunctorπ for the natural quotient from ambient
singular chains. These definitions compose the topological singular-pair
functor with Mathlib's SSetPair functors, whose cokernel construction supplies
the categorical quotient behavior. The elementwise description of the
connecting map is recorded with the integral long exact sequence rather than
imposed on arbitrary coefficient categories.
Sources
Dependencies
Exact sequences and homotopy invariance
Hatcher, Theorem 2.16 (pages 116–117). A short exact sequence of chain complexes in an abelian category induces an exact long sequence in homology, with connecting maps lowering degree by one.
The pinned theorem
HomologicalComplex.HomologySequence.composableArrows₅_exact proves the
exactness of every consecutive six-object segment. Together with its
degree parameters, these segments are Hatcher's long exact sequence. The
connecting morphism and the three local exactness statements are supplied by
CategoryTheory.ShortComplex.ShortExact.δ and
homology_exact₁/₂/₃ in the same API.
For a complex indexed by ℕ, the six-object theorem does not itself express
the terminal epimorphism into degree-zero homology. The pinned supporting
lemma HomologicalComplex.epi_homologyMap_of_epi_of_not_rel supplies that
endpoint when there is no lower degree; the pair-specific API exposes the
corresponding Epi instance for its degree-zero relative-chain projection.
Dependencies
Hatcher, §2.1 (page 117). For a topological pair (X,A), the inclusion,
the map induced by the relative-chain quotient, and the connecting maps form
an exact sequence
... → Hₙ(A;R) → Hₙ(X;R) → Hₙ(X,A;R) → Hₙ₋₁(A;R) → ....
Hatcher.Relative.pairSequence packages six consecutive terms, while
Hatcher.Relative.pairSequence_exact proves exactness at every position,
uniformly over adjacent degrees. Hatcher.Relative.pairConnecting exposes the
connecting morphism, and Hatcher.Relative.pairConnecting_eq proves that it
sends a relative cycle represented by α to the homology class of ∂α. In
the integral AddCommGrpCat specialization, generalized elements from ℤ
recover the source's elementwise formula δ[α] = [∂α].
Hatcher, §2.1 (page 127). A map of topological pairs induces a morphism between their long exact homology sequences. In particular it commutes with the inclusion maps, the maps induced by the relative-chain quotients, and the connecting homomorphisms.
Hatcher.Relative.pairSequenceMap packages the induced morphism between six
consecutive terms. Naturality of the ordinary and relative homology functors
supplies its inclusion and quotient squares, while
Hatcher.Relative.pairConnecting_naturality proves the substantive square
containing the connecting morphism.
Sources
For homotopic maps of topological pairs, descend the compatible singular-chain homotopies on the ambient spaces and subspaces through the relative-chain cokernels. The result is a chain homotopy between the induced maps on relative singular chain complexes.
Hatcher.Relative.chainHomotopyOfPairHomotopy carries this out degreewise by
the cokernel universal property. It first proves that the ambient and subspace
singular-chain homotopies commute with the inclusions, then descends the
ambient homotopy to the relative quotient. This compatibility is essential:
an unrelated pair of absolute chain homotopies does not define a map on the
quotient complex.
Sources
Hatcher, Proposition 2.19 (page 118). If two maps
f,g : (X,A) ⟶ (Y,B) are homotopic through maps of pairs, then they induce
the same map Hₙ(X,A;R) ⟶ Hₙ(Y,B;R) in every degree.
Hatcher.Relative.congr_homologyMap applies chain-homotopy invariance to the
compatible relative chain homotopy constructed by
Hatcher.Relative.chainHomotopyOfPairHomotopy. The proof therefore descends
the explicit ambient and subspace homotopies to relative chains before passing
to homology; it does not treat the HomologyPretheory.IsHomotopyInvariant
interface as a proof of the result.
Hatcher, §2.1 (page 118). For a topological pair (X,A) with nonempty
subspace, replace the two absolute homology terms in the pair long exact
sequence by reduced homology while retaining the same relative groups. The
resulting sequence is exact in every degree.
Hatcher.Relative.reducedPairSequence packages six consecutive terms and
Hatcher.Relative.reducedPairSequence_exact proves their exactness. The
construction uses the short exact sequence of augmented subspace and ambient
chains together with the zero-augmented relative complex. For a chosen point
of the nonempty subspace, Hatcher.Relative.reducedPairZeroSequence_exact
also proves the terminal exact sequence
H̃₀(A) → H̃₀(X) → H₀(X,A) → 0 directly from the augmentation.
The overlap lemmas identify these finite windows as one coherent sequence, and
Hatcher.Relative.reducedPairLongExact packages all exactness conclusions.
Sources
Dependencies
Hatcher, §2.1 (pages 127–128). A map of topological pairs with nonempty subspaces induces a morphism between their reduced long exact homology sequences, commuting in particular with the connecting homomorphisms.
Hatcher.Relative.reducedPairSequenceMap packages the induced morphism between
six consecutive terms. The main theorem
Hatcher.Relative.reducedPairConnecting_naturality proves the connecting
square directly from the natural augmented-chain construction, including in
degree zero. It does not transport naturality through a chosen-point splitting
of zeroth homology, since that splitting is not natural for unpointed spaces.
Sources
Hatcher, Example 2.18 (page 118). For a space X with chosen point x₀,
construct an isomorphism
Hₙ(X,{x₀};R) ≅ H̃ₙ(X;R) for every degree n.
Hatcher.Relative.pointedPairHomologyIso constructs this comparison from the
reduced long exact sequence and the vanishing of reduced homology of a point.
It includes degree zero rather than only the positive-degree case.
Dependencies
Triple exact sequence
For nested subspaces B ⊆ A ⊆ X, bundle the composable embeddings
B ↪ A ↪ X as a topological triple (X,A,B). It determines the three
topological pairs (A,B), (X,B), and (X,A), together with the canonical
maps of pairs
(A,B) → (X,B) → (X,A).
Define a morphism of triples by compatible maps on all three spaces, and expose
the induced morphisms of these pairs. The main declaration is
Hatcher.Relative.TopTriple; its morphism and pair projections are supporting
definitions in the same review unit.
Sources
For a topological triple (X,A,B) and coefficients R, the canonical maps of
relative singular chain complexes form a short exact sequence
0 → C_*(A,B;R) → C_*(X,B;R) → C_*(X,A;R) → 0.
The main theorem Hatcher.Relative.tripleChainComplexShortComplex_shortExact
proves short exactness. The short complex itself and its functorial maps are
supporting declarations. Its proof uses the cokernel tail of Mathlib's
kernelCokernelCompSequence and the existing universal properties of relative
chains, rather than copying the unmerged basis-splitting implementation from
Mathlib PR #41318.
Sources
Dependencies
Hatcher, §2.1 (pages 118–119). For nested subspaces B ⊆ A ⊆ X, the
relative groups fit into a long exact sequence
⋯ → H_n(A,B;R) → H_n(X,B;R) → H_n(X,A;R)
→ H_{n-1}(A,B;R) → H_{n-1}(X,B;R) → ⋯.
For adjacent degrees m + 1 = n, Hatcher.Relative.tripleSequence packages
six consecutive terms and Hatcher.Relative.tripleSequence_exact proves
exactness at every position. The same review unit exposes the connecting map
and Hatcher.Relative.tripleHomologyMapXBToXA_zero_epi proves the degree-zero
epimorphism H_0(X,B;R) → H_0(X,A;R).
Sources
Dependencies
Hatcher, §2.1 (page 128). A map of triples induces a morphism between their long exact homology sequences. The maps on the three relative terms commute with the inclusion, quotient, and connecting morphisms.
Hatcher.Relative.tripleSequenceMap packages the induced morphism between six
consecutive terms. The main theorem
Hatcher.Relative.tripleConnecting_naturality proves the substantive square
containing the connecting morphism; the remaining squares follow from
functoriality of relative homology.
Dependencies
Small chains and excision
Good pairs and quotient exact sequences
Post-excision applications
Decomposed and deferred boundary
Theorem 2.20 and its Proposition 2.21 small-chain machinery are decomposed in the milestone above, and all ten leaves are complete. Theorem 2.13, Proposition 2.22, and their naturality are formalized locally and complete in the good-pair milestone. The arbitrary-pair mapping-cone comparison, Example 2.23, Corollaries 2.24–2.25, and invariance of dimension are formalized and complete in the post-excision milestone. Example 2.17 and the simplicial–singular comparison remain deferred.