Post-excision applications
Hatcher §2.1, printed pages 125–126. This milestone begins immediately after Proposition 2.22 and uses the completed relative-homology, excision, good-pair, and sphere-homology APIs. It covers the arbitrary-pair mapping-cone comparison, the explicit fundamental cycles of Example 2.23, CW-subcomplex excision and wedge additivity in Corollaries 2.24–2.25, and invariance of dimension in Theorem 2.26.
The milestone has twenty-seven §2.1 leaves. Five separate Appendix leaves construct the Proposition A.5 regular neighborhoods needed by Corollary 2.24. All thirty-two leaves are formalized locally and complete. Theorem 2.27, degree, cellular homology, and homology with coefficients remain outside this boundary.
Arbitrary-pair mapping cones
Hatcher, §2.1 (page 125). For a topological pair
P : TopPair, representing an embedding P.map : P.snd ⟶ P.fst, define its
mapping cone X ∪ CA by attaching the cone
CA = (A × I) / (A × {0}) to X along the copy of A at height one.
The main declaration is
Hatcher.Relative.mappingCone (P : TopPair.{w}) : TopCat.{w}.
Use the existing explicit point-set model
Hatcher.VanKampen.ConeAttachment P.map: height zero is collapsed to its
distinguished apex, and height one is glued to P.fst through P.map. The
existing pushout theorem must witness that this is the topological mapping
cone, rather than an opaque homeomorphic replacement. Retain the explicit apex
when P.snd is empty; then the model is P.fst ⊔ point, which makes the
degree-zero reduced comparison in the final theorem valid without a
nonemptiness hypothesis.
In the same formalization unit, expose the standard two-set cover under the
relative-homology namespace. Define mappingConeUpperPair P to be the pair
whose subspace is the contractible upperCover, and define
mappingConeCoverPair P to be (lowerCover, upperCover ∩ lowerCover).
Package the two open sets as mappingConeCoverCondition P with upperCover
as the first subset and lowerCover as the second. Finally define the
canonical excision morphism
Hatcher.Relative.mappingConeExcision P :
mappingConeCoverPair P ⟶ mappingConeUpperPair P
to be Hatcher.Excision.coverPairHom (mappingConeCoverCondition P). These
supporting definitions must retain the exact canonical inclusion used by the
existing binary-cover excision theorem. No mapping-cone functor or naturality
claim is part of this node.
Sources
Let P : TopPair.{w} have contractible subspace P.snd. For an object R in
an abelian category with the coproducts required by singular chains, construct
in every degree n an isomorphism
Hatcher.Relative.contractibleSubspaceHomologyIso P R n :
(Hatcher.Reduced.homologyFunctor R n).obj P.fst ≅
(Hatcher.Relative.homologyFunctor R n).obj P.
The forward morphism must be exactly
Hatcher.Relative.reducedPairProjection P R n, not an unspecified isomorphism.
First prove the supporting instance
Hatcher.Relative.reducedPairProjection_isIso_of_contractibleSubspace and
define the displayed isomorphism with asIso.
This is the reusable exact-sequence step behind the first isomorphism on
Hatcher page 125. Reduced homology of the contractible subspace vanishes in
all degrees. For positive-degree windows, exactness makes the reduced-pair
projection both monic and epic; degree zero must use the separately formalized
terminal sequence
H̃₀(P.snd) ⟶ H̃₀(P.fst) ⟶ H₀(P) ⟶ 0.
The contractibility assumption already supplies nonemptiness, so do not add a
redundant chosen point or strengthen the topological hypotheses.
Sources
Dependencies
For P : TopPair, construct a morphism of topological pairs
Hatcher.Relative.mappingConeCoverRetraction P :
mappingConeCoverPair P ⟶ P.
Its ambient component is the existing retraction from the mapping cone's
lowerCover to P.fst. Its subspace component is an explicit projection
upperCover ∩ lowerCover ⟶ P.snd obtained from the open interior cylinder.
The two components must commute strictly with the pair embeddings: on an
interior cylinder point represented by (a,t), the ambient retraction is
P.map a, while the subspace projection is a.
The main declaration is the instance
Hatcher.Relative.mappingConeCoverRetraction_homologyMap_isIso
stating, for every coefficient object R in an abelian category with the
required coproducts and every n : ℕ, that
IsIso ((Hatcher.Relative.homologyFunctor R n).map
(Hatcher.Relative.mappingConeCoverRetraction P)).
Expose a homotopy equivalence whose forward map is exactly the chosen
intersection projection. Do not rely on unfolding the opaque choice inside
the existing intersection equivalence. The ambient and subspace components
then induce ordinary homology isomorphisms, and the completed componentwise
relative-homology criterion supplies the stated instance, including degree
zero. This node does not assert a new homeomorphism or a homotopy equivalence
in the category TopPair.
Sources
Dependencies
Hatcher, §2.1 (page 125). For every topological pair P, coefficient
object R in an abelian category with the coproducts required by singular
chains, and degree n : ℕ, construct the isomorphism
Hatcher.Relative.mappingConeHomologyIso P R n :
(Hatcher.Relative.homologyFunctor R n).obj P ≅
(Hatcher.Reduced.homologyFunctor R n).obj
(Hatcher.Relative.mappingCone P).
This includes degree zero and imposes no good-pair, closedness, or nonemptiness
hypothesis. Hatcher's integral statement is the specialization to
AddCommGrpCat.of ℤ.
Let D := mappingConeCoverPair P, Q := mappingConeUpperPair P,
F := Hatcher.Relative.homologyFunctor R n,
r := mappingConeCoverRetraction P, and e := mappingConeExcision P. Let
κ := contractibleSubspaceHomologyIso Q R n, oriented from reduced ambient
homology to relative homology. Define the main isomorphism by the exact
composition
(asIso (F.map r)).symm ≪≫ asIso (F.map e) ≪≫ κ.symm.
Expose a simplification lemma for its inverse identifying it with
Hatcher.Relative.reducedPairProjection Q R n ≫
inv (F.map e) ≫ F.map r.
Thus the source-order direction is precisely Hatcher's sequence: reduced
homology of the mapping cone maps to relative homology against the
contractible cone-side member; excision removes the apex-side neighborhood;
and the punctured pair retracts to (X,A). Do not replace any of these
canonical morphisms by an unspecified isomorphism, and do not add functoriality
or naturality beyond the printed-page-125 claim.
Sources
Dependencies
Explicit simplex and sphere classes
For the ordered topological simplex Δ[n] :=
Convexity.StdSimplex ℝ (Fin (n + 1)), define its boundary by the vanishing
of at least one barycentric coordinate. In Δ[n+1], define the zero horn as
the union of every codimension-one face except face zero. Package the
inclusions
Λ⁰[n+1] ⊆ ∂Δ[n+1] ⊆ Δ[n+1]
as a Hatcher.Relative.TopTriple, and package the zero-face map as a morphism
of pairs
(Δ[n], ∂Δ[n]) ⟶ (∂Δ[n+1], Λ⁰[n+1]).
The main artifact is Hatcher.Simplex.standardSimplexBoundaryHornTriple.
Supporting definitions include the relative simplex pair and the identity
singular simplex obtained from TopCat.toSSetObjEquiv.
These are topological standard simplices and singular chains. Do not replace them by simplicial-set homology, since the comparison with singular homology is Theorem 2.27 and lies beyond this milestone.
Sources
Dependencies
Construct a strong deformation retraction of Δ[n+1] onto Λ⁰[n+1].
In barycentric coordinates, subtract the minimum of the coordinates with
positive index, transfer the removed mass to coordinate zero, and interpolate
linearly from the identity. Prove continuity, preservation of the simplex,
the endpoint formula, and pointwise fixation of the horn.
The main artifact is
Hatcher.Simplex.zeroHornStrongDeformationRetract. It supplies the vanishing
of H_*(Δ[n+1], Λ⁰[n+1];R) used in the triple-sequence induction of Example
2.23.
Sources
For a positive-dimensional standard simplex, construct chosen good-pair data
for (Δ[n], ∂Δ[n]). Use the complement of the barycenter as a neighborhood
of the boundary and radial normalization away from that barycenter.
For (∂Δ[n+1], Λ⁰[n+1]), remove the barycenter of the omitted zero face and
retract the remaining boundary onto the horn by subtracting and renormalizing
the least positive-index barycentric coordinate. The retraction must fix the
horn pointwise.
The main artifact is
Hatcher.Simplex.boundaryZeroHornGoodPairData; the simplex-boundary witness
is supporting data. State the positive-dimensional restriction explicitly:
the boundary of Δ[0] is empty, while the project's GoodPairData requires a
nonempty subspace.
Sources
Show that the square formed by the boundary of the zero face, the zero face,
the zero horn, and the full boundary is a pushout in TopCat:
∂Δ[n] → Δ[n]
↓ ↓
Λ⁰[n+1] → ∂Δ[n+1].
Use pushout pasting to construct the resulting isomorphism between point
quotients. The main artifact is
Hatcher.Simplex.zeroFacePointQuotientIso. Its forward map must be the
functorial pointQuotientMap induced by the canonical zero-face morphism of
pairs.
The proof uses the finite closed-cover gluing property of the face and horn; it must not appeal to the later simplicial-versus-singular comparison.
Sources
For every n : ℕ, prove that the canonical zero-face map induces an isomorphism
H_n(Δ[n], ∂Δ[n];R) ≅ H_n(∂Δ[n+1], Λ⁰[n+1];R).
The main artifact is
Hatcher.Simplex.zeroFacePair_homologyMap_isIso, stated for every homological
degree for which the canonical pair map is an isomorphism. For n > 0, use
the good-pair comparisons and the exact point-quotient isomorphism. Handle
n = 0 directly: the source boundary is empty, so Proposition 2.22's local
GoodPairData interface does not apply. The direct branch must still prove
that the canonical map, rather than an arbitrary conjugate, is an isomorphism.
Formalized in Hatcher/Singular/StandardSimplexZeroFaceHomology.lean for an
arbitrary coefficient object in an abelian category with the required
coproducts, and for every simplex dimension and homological degree. In positive
simplex dimensions, naturality of the good-pair quotient comparison conjugates
the canonical relative-homology map to the reduced-homology map induced by
zeroFacePointQuotientIso; the theorem identifying that isomorphism's forward
map ensures this is the exact zero-face map. In dimension zero, the two endpoint
subspaces form an open binary cover of ∂Δ[1]. The canonical pair map factors
as a source pair isomorphism, the binary-cover excision map, and a target pair
isomorphism, so this exceptional branch also proves that exact map is an
isomorphism.
Sources
Dependencies
Give the connecting morphism in the long exact sequence of a topological
triple its chain-level formula. If a cycle in C_n(X,A;R) is lifted to
C_n(X,B;R) and its boundary is represented in C_{n-1}(A,B;R), prove that
Hatcher.Relative.tripleConnecting sends the original homology class to the
class of that boundary.
The main artifact is Hatcher.Relative.tripleConnecting_eq, parallel to the
existing pairConnecting_eq. Include the categorical criterion that this
connecting map is an isomorphism when the two adjacent groups
H_n(X,B;R) and H_{n-1}(X,B;R) vanish.
This node is generic triple-sequence infrastructure. Example 2.23 uses it to identify the image of the ordered identity simplex, not merely to know that some connecting isomorphism exists.
Hatcher.Relative.tripleConnecting_eq states the formula with the relative
cycle, its lift, and the boundary representative as explicit chain-level data;
the resulting equality has coefficient +1. The companion theorem
Hatcher.Relative.tripleConnecting_isIso shows that the connecting morphism
is an isomorphism when the adjacent groups H_n(X,B;R) and
H_{n-1}(X,B;R) vanish.
Sources
Hatcher, Example 2.23 (printed page 125). Regard the identity map of the
ordered topological simplex Δ[n] as a singular n-simplex. Its boundary
lies in ∂Δ[n], so it defines a canonical class morphism
R ⟶ H_n(Δ[n], ∂Δ[n];R).
Define this morphism as
Hatcher.Simplex.relativeSimplexFundamentalClass R n using the actual
singular-chain inclusion, relative-chain projection, cycle lift, and homology
projection. Prove
theorem Hatcher.Simplex.relativeSimplexFundamentalClass_isIso :
IsIso (relativeSimplexFundamentalClass R n)
by induction on n. In the successor step use the triple
(Δ[n+1], ∂Δ[n+1], Λ⁰[n+1]). Choose face zero as the omitted face, so the
surviving term of the alternating boundary has coefficient +1; no hidden
orientation sign may be absorbed into an arbitrary isomorphism. The integral
specialization says that the identity simplex represents a generator of the
infinite cyclic relative group.
Formalized in Hatcher/Singular/RelativeSimplexFundamentalClass.lean for an
arbitrary coefficient object in an abelian category with the required
coproducts. The degree-zero case identifies the unique simplex chain and the
empty-boundary quotient directly. The successor step applies the triple
connecting map to the identity simplex; every positive-index face vanishes in
the zero-horn quotient, while face zero survives with coefficient +1 and is
the canonical zero-face image of the lower-dimensional identity class.
Sources
Dependencies
Construct an isomorphism of topological pairs between the ordered standard simplex and Mathlib's standard disk:
(Δ[n], ∂Δ[n]) ≅ (TopCat.disk n, TopCat.diskBoundary n).
The main artifact is Hatcher.Simplex.standardSimplexPairIsoDiskPair. Build
it from an explicit affine-hyperplane model followed by radial gauge
rescaling, and prove that the boundary is carried to the unit sphere. Cover
n = 0, where both boundaries are empty.
This is the precise equivalence used when Hatcher replaces
(D^n, ∂D^n) by (Δ^n, ∂Δ^n). It may transport the ordered simplex
fundamental class to the disk pair, but it must not claim a canonical
Euclidean orientation unless the chosen homeomorphism proves that stronger
compatibility.
Sources
Dependencies
Define the double-simplex space Hatcher.Simplex.doubleSimplex n as the
TopCat pushout of two copies of Δ[n] along their boundaries, using the
same ordering of boundary vertices on both copies. Let σ₁ and σ₂ be the
two singular n-simplices induced by the pushout inclusions.
Define
Hatcher.Simplex.doubleSimplexFundamentalCycle R n
to be the augmented singular chain σ₁ - σ₂. Prove it is a cycle: each face
of σ₁ equals the corresponding face of σ₂ by the pushout relation, so the
boundaries cancel term by term. The construction includes n = 0, where the
augmentation of the difference is zero.
This node records the exact cycle from Hatcher's Example 2.23. It does not yet prove that the resulting reduced-homology class is a generator.
Sources
Dependencies
Let D_n be the double-simplex space and let its second simplex be the
distinguished subspace. Construct a collar neighborhood showing that this
second summand forms a good pair with D_n. Define the canonical map of pairs
(Δ[n], ∂Δ[n]) ⟶ (D_n, Δ[n]_2)
whose ambient component is the first pushout inclusion and whose subspace component is the common boundary viewed in the second simplex.
The main theorem
Hatcher.Simplex.doubleSimplexFirstPair_homologyMap_isIso says that this
canonical map induces an isomorphism on relative homology in every degree.
For positive dimension, identify its point-quotient map by pushout pasting and
apply Proposition 2.22. Treat dimension zero directly, since the source
subspace is empty and hence is not accepted by the project's GoodPairData.
Sources
Dependencies
Lift doubleSimplexFundamentalCycle R n to a named class morphism
R ⟶ H̃_n(doubleSimplex n;R)
and prove that this exact morphism is an isomorphism. The main artifacts are
Hatcher.Simplex.doubleSimplexFundamentalClass and
Hatcher.Simplex.doubleSimplexFundamentalClass_isIso.
Use the reduced-to-relative comparison for the pair consisting of the double
simplex and its contractible second summand, followed by the canonical
relative comparison from the first simplex. Prove at chain level that the
difference cycle maps to the identity simplex: the second summand vanishes in
the relative quotient and the first remains. The integral specialization
therefore says that Δ₁^n - Δ₂^n, with the common vertex ordering, is a
generator rather than merely that the group is abstractly cyclic.
Formalized in Hatcher/Singular/DoubleSimplexFundamentalClass.lean. The
definition lifts the literal ordered difference cycle to augmented homology.
Its canonical projection relative to the second simplex is proved, at chain
level, to be the image of the identity simplex from the first summand; the
relative-simplex generator theorem and both canonical comparison isomorphisms
then prove the named class is an isomorphism in every dimension, including
dimension zero.
Sources
Dependencies
Construct a homeomorphism
Hatcher.Simplex.doubleSimplex n ≅ TopCat.sphere n.
The main artifact is Hatcher.Simplex.doubleSimplexIsoSphere. First carry
each standard simplex to a closed disk by the simplex-pair homeomorphism, then
identify the double of the disk along its boundary with the standard unit
sphere. The two disk maps must agree on the common boundary so that the
homeomorphism descends from the pushout.
The formalization uses the explicit hemisphere parametrizations
x ↦ (x, ±√(1 - ‖x‖²)). Their first coordinates recover x, their final
coordinates agree on the unit sphere, and every target point lies in one of
the two images. This works uniformly in dimension zero. Compactness of the
disk pushout then upgrades the continuous bijection to a homeomorphism.
Transport the double-simplex fundamental class across this homeomorphism and record that the transported class morphism is an isomorphism. Keep the ordered double-simplex class as the source-facing orientation datum: the existing sphere calculation returns only a nonempty type of isomorphisms and does not identify Hatcher's named cycle.
The transported class is
Hatcher.Simplex.doubleSimplexSphereFundamentalClass, and
Hatcher.Simplex.doubleSimplexSphereFundamentalClass_isIso proves that it is
a generator. Transporting it back along the inverse homeomorphism recovers
the literal ordered difference class.
Sources
CW subcomplexes
Hatcher, Corollary 2.24 (printed page 126). Let a classical CW complex
C be the union of subcomplexes A and B. Define the canonical inclusion
of topological pairs
(B, A ∩ B) ⟶ (C, A)
and prove that it induces an isomorphism on relative singular homology in
every degree. The main artifacts are
Hatcher.ClassicalCW.subcomplexExcisionPairHom and
Hatcher.ClassicalCW.subcomplexExcision_homologyMap_isIso.
Use the compatible regular neighborhoods supplied by Appendix Proposition
A.5. Enlarge (B,A ∩ B) to (N(B),N(A) ∩ N(B)), apply binary-cover
excision to (N(B),N(A) ∩ N(B)) → (C,N(A)), and compare (C,A) with
(C,N(A)) through the strong deformation retraction. Identify the resulting
composite with the displayed canonical pair map.
This route includes A ∩ B = ∅. Do not use only Proposition 2.22 for the
final theorem, since the project's good-pair structure deliberately requires
a nonempty subspace.
Sources
Dependencies
Wedge additivity
For a family of pointed spaces (X i, x₀ i), define the topological pair
(Σ i, X i ; Σ i, {x₀ i})
whose structure map sends ⟨i, unit⟩ to ⟨i, x₀ i⟩. The main artifact is
Hatcher.Relative.sigmaPointedPair. For every index i, expose the canonical
map from pointedPair (X i) (x₀ i) to the sigma pair and prove its component
formulas.
The construction uses the ordinary topological sigma type, which is the
coproduct in TopCat. It includes the empty family: then both the ambient and
subspace of the sigma pair are empty.
Sources
Dependencies
Construct a chain-complex isomorphism from the categorical coproduct of the relative singular chain complexes of a family of pairs to the relative chain complex of their sigma pair. Specialize the public interface to the family of pointed pairs used for wedge sums:
∐ i, C_*(X_i,{x_i};R) ≅ C_*(Σ i, X_i; Σ i,{x_i};R).
The main artifact is
Hatcher.Relative.relativeChainComplexSigmaIso. Its component on every
summand must be the chain map induced by the canonical sigma inclusion.
Use ContinuousMap.sigmaCodHomeomorph: the topological standard simplex is
connected, so every singular simplex in a disjoint union lands in one unique
summand. Prove that this equivalence commutes with every face map and hence
with the alternating differential.
Sources
Assume the coefficient category has exact coproducts of the size of the index
type, expressed by Mathlib's AB4OfSize interface. Construct the natural
isomorphism
∐ i, H_n(P_i;R) ≅ H_n(Σ P_i;R)
whose forward map restricts on each coproduct summand to the relative-homology
map induced by the corresponding sigma inclusion. The main artifact is
Hatcher.Relative.relativeHomologySigmaIso.
Derive the result from relativeChainComplexSigmaIso and exactness of the
coproduct functor. Do not state this under only [Abelian C] and
[HasCoproducts C]: infinite coproducts need not preserve homology in an
arbitrary abelian category. Mathlib supplies the required AB4 instance for
AddCommGrpCat, which covers Hatcher's integral statement.
Sources
Let the index type be nonempty and suppose every pointed pair
(X i,{x₀ i}) is good. Prove that their sigma pair is good:
theorem Hatcher.Relative.sigmaPointedPair_isGoodPair
[Nonempty ι]
(h : ∀ i, IsGoodPair (pointedPair (X i) (x₀ i))) :
IsGoodPair (sigmaPointedPair x₀)
Assemble the chosen neighborhoods fiberwise. Prove the basepoint sigma range
lies in the interior of the assembled sigma neighborhood, prove the sigma of
the closed basepoint images is closed, and assemble the pointwise strong
deformation retractions into one sigma deformation. The nonempty-index
assumption supplies the nonempty subspace required by GoodPairData.
Keep the empty-index case out of this theorem. It is handled directly by the contractibility of the project's empty pointed wedge in Corollary 2.25.
Sources
Identify the existing project model Hatcher.PointedWedge X x₀ with the
point quotient of sigmaPointedPair x₀. Prove that the square from the sigma
of the chosen basepoints to the sigma of the spaces and to PUnit is a
pushout in TopCat, then construct
Hatcher.Relative.pointQuotientSigmaPointedPairIsoPointedWedge.
The isomorphism must carry the quotient point to
Hatcher.PointedWedge.basepoint x₀, and the quotient projection restricted to
summand i to Hatcher.PointedWedge.inclusion x₀ i. Include these as public
simp lemmas so the final homology map can be identified with Hatcher's direct
sum of inclusion-induced maps.
The construction includes the empty family: the point quotient of the empty pair and the project's empty wedge are both one-point spaces.
Sources
Hatcher, Corollary 2.25 (printed page 126). For a family of pointed
spaces (X i,x₀ i), define the canonical morphism
Hatcher.PointedWedge.reducedHomologyCoproductMap X x₀ R n :
(∐ i, H̃_n(X i;R)) ⟶ H̃_n(PointedWedge X x₀;R)
as Sigma.desc of the reduced-homology maps induced by the canonical summand
inclusions. If every pointed pair (X i,{x₀ i}) is good and the relevant
coproducts are exact, prove that this exact morphism is an isomorphism. The
main theorem is
Hatcher.PointedWedge.reducedHomologyCoproductMap_isIso.
For a nonempty family, compare pointed relative homology summandwise, use the relative-homology coproduct isomorphism, apply Proposition 2.22 to the sigma good pair, and identify its point quotient with the existing wedge. Use the completed naturality theorems to prove that the resulting composite is the displayed canonical map. For an empty family, prove the result directly from the contractibility of the empty pointed wedge and the initial empty coproduct.
Expose an integral specialization with no explicit AB4 hypothesis; this is Hatcher's direct sum of abelian groups.
Sources
Dependencies
Local homology and dimension
- Local homology is unchanged on an open neighborhood
- Relative homology in a contractible ambient space
- Local homology of positive-dimensional Euclidean space
- Homeomorphic nonempty Euclidean open sets have equal dimension