Skip to content

Computations and applications

Hatcher §2.2 (pages 134–159), together with the selected sphere applications from §2.1. The binary interior-cover Mayer–Vietoris sequence is complete in six formalizable leaves. The thirteen-leaf continuation covering neighborhood-retract transport, Example 2.46, and reduced sphere homology is also complete. The three-leaf Corollary 2.15 application is complete. The dependency-ordered branches formalize the §2.1 post-excision applications through Theorem 2.26 in twenty-seven leaves, supported by five Appendix A.5 regular-neighborhood leaves. All thirty-two are complete. The remainder of §2.2 now also has a sixteen-leaf degree-foundations milestone through Proposition 2.29. All sixteen leaves are formalized locally and complete; the local-degree continuation through Proposition 2.30 is decomposed into twenty leaves, twelve formalized locally and eight remaining. The later material stays explicitly deferred.

Given excision and the long exact sequence, homology becomes computable. From Hₙ(Sⁿ) ≅ ℤ comes the degree of a map Sⁿ → Sⁿ, with its local formula as a sum over preimages, which settles the hairy ball theorem and which finite groups act freely on spheres. Cellular homology computes Hₙ of a CW complex from its cells and attaching maps, reducing infinite singular chain groups to finitely generated ones. Mayer–Vietoris is the homology analogue of van Kampen. The section closes with coefficients in an arbitrary abelian group.

The selected Corollary 2.15 branch derives Brouwer's fixed-point theorem for all positive-dimensional disks, generalizing the two-dimensional case proved from π₁(S¹) in basic constructions. Invariance of domain belongs to out-of-scope Additional Topic §2.B.

The completed Mayer–Vietoris milestone constructs the ordinary and reduced exact sequences directly from the completed small-chain equivalence. The completed sphere-homology milestone adds the conditional neighborhood-retract extension, applies it to the hemispheres of a sphere, and continues through the completed no-retraction and Brouwer applications.

The post-excision applications branch continues from Proposition 2.22 through mapping cones, explicit fundamental cycles, CW-subcomplex excision, and wedge additivity. The separate local-homology branch culminates in Theorem 2.26. These pages retain their §2.1 source binding but are placed here so their sphere-homology prerequisites remain dependency-ordered.

The degree-foundations milestone uses the completed ordered sphere class to define degree, calculate reflections and the antipodal map, prove the fixed-point-free formula, and reach Theorem 2.28 and Proposition 2.29. The local-degree milestone then orients local homology, constructs the finite-puncture direct sum, and continues toward Proposition 2.30; twelve of its twenty leaves are complete.

The pinned Mathlib supplies the standard disk, boundary, and inclusion models, but not the selected no-retraction, Brouwer, sphere-homology, degree, or Mayer–Vietoris results. It has CW complexes but no cellular homology or degree theory; its MayerVietoris files are sheaf-theoretic and unrelated. External prior art is recorded in the implementation specifications but is neither pinned Mathlib coverage nor a project dependency.

Selected milestones

Degree-realization examples, suspension invariance, cellular homology, the later Mayer–Vietoris applications, and homology with general coefficient groups as a separate source topic remain deferred.

Sources