Mayer–Vietoris transport, sphere homology, and Brouwer

Hatcher §2.1, printed pages 109–115, and §2.2, printed page 150. This milestone transports the completed Mayer–Vietoris sequences across supplied neighborhood deformation retractions, applies the reduced sequence to the northern and southern hemispheres, and derives the reduced homology of every sphere. Its final branch applies that calculation to Corollary 2.15.

The public result uses Mathlib's TopCat.sphere and remains general in the coefficient object. Hatcher's integral Corollary 2.14 is an explicit specialization. The recurrence follows Example 2.46 rather than the separately decomposed good-pair quotient proof that originally precedes Corollary 2.14.

For Corollary 2.15, Mathlib's TopCat.disk, TopCat.diskBoundary, and TopCat.diskBoundaryInclusion give the exact standard pair. The homological no-retraction argument and the fixed-point-free boundary-ray construction are independent branches; Brouwer's theorem joins them.

Formalization progress

6 definitions · 10 results

16 fully proved

Reduced homotopy invariance

Theorem74Homotopic maps induce the same reduced-homology map#✓fully proved

Let C have a category structure, coproducts, a preadditive structure, and homology. For maps f g : X ⟶ Y in TopCat, a coefficient object R : C, and a homotopy from f to g, prove that the two morphisms induced on reduced homology agree in every degree:

(Hatcher.Reduced.homologyFunctor R n).map f = (Hatcher.Reduced.homologyFunctor R n).map g.

The main result is Hatcher.Reduced.homologyMap_eq_of_homotopy. Supporting declarations should lift augmentation-compatible chain maps and chain homotopies through ChainComplex.augment in a neutral module. This avoids importing the higher-level excision development merely to reuse its current private helper.

Sources

• Hatcher §2.1, reduced induced maps and homotopy invariance, pages 111–113
• Sphere-homology implementation specification

Dependencies

Statement usesDefinition 65 (Reduced singular homology)

Proof usesDefinition 76 (A topological homotopy gives a singular-chain homotopy) · Lemma 6 (Chain-homotopic maps induce the same homology map)

Used byDefinition 85 (A homotopy equivalence induces reduced-homology isomorphisms)

Definition85A homotopy equivalence induces reduced-homology isomorphisms#✓fully proved

Let C have a category structure, coproducts, a preadditive structure, and homology. For a homotopy equivalence e : X ≃ₕ Y, a coefficient object R : C, and a degree n, construct an isomorphism

H̃_n(X;R) ≅ H̃_n(Y;R).

The main artifact is Hatcher.Reduced.homologyIsoOfHomotopyEquiv. Its forward morphism must be the map induced by e.toFun, with a public simplification lemma parallel to the ordinary singular-homology API. Construct the inverse from e.invFun and use reduced homotopy invariance for the inverse laws.

Sources

• Hatcher §2.1, Corollary 2.11 and the reduced analogue, pages 111–113
• Sphere-homology implementation specification

Dependencies

Statement usesDefinition 65 (Reduced singular homology)

Proof usesTheorem 74 (Homotopic maps induce the same reduced-homology map)

Used byTheorem 109 (Local homology of positive-dimensional Euclidean space) · Theorem 75 (Reduced homology of a contractible space vanishes) · Theorem 105 (The reduced neighborhood-retract Mayer–Vietoris sequence)

Theorem75Reduced homology of a contractible space vanishes#✓fully proved

Let C be an abelian category with the required coproducts, [ContractibleSpace X], and R : C. For every n : ℕ, prove

IsZero ((Hatcher.Reduced.homologyFunctor R n).obj (TopCat.of X)).

The main result is Hatcher.Reduced.isZero_homology_of_contractible. Transport reduced homology along a contraction equivalence with a point and use the existing reduced point calculation.

Sources

• Hatcher §2.1, reduced homology of contractible spaces, page 111
• Sphere-homology implementation specification

Dependencies

Statement usesDefinition 65 (Reduced singular homology)

Proof usesDefinition 85 (A homotopy equivalence induces reduced-homology isomorphisms) · Definition 74 (Relative homology at a basepoint is reduced homology)

Used byTheorem 85 (A nonsurjective sphere map has degree zero) · Definition 105 (Relative homology in a contractible ambient space) · Definition 86 (A contractible subspace identifies reduced and relative homology) · Corollary 3 (Reduced homology of a wedge is the direct sum of the summands) · Theorem 113 (The boundary sphere is not a retract of the disk) · Theorem 106 (The reduced homology of spheres satisfies the suspension recurrence)

Neighborhood transport

Theorem102The ordinary neighborhood-retract Mayer–Vietoris sequence#✓fully proved

Let C be an abelian category with the coproducts required by the completed Mayer–Vietoris API, and let R : C. For subsets A B : Set X, package the structure Hatcher.MayerVietoris.NeighborhoodCover A B, with neighborhoods U V : Set X as fields, from the following data: A ∪ B = Set.univ, A ⊆ interior U, B ⊆ interior V, and strong deformation retractions along the subtype inclusions from U to A, from V to B, and from U ∩ V to A ∩ B. The neighborhood hypotheses must produce Hatcher.Excision.CoverCondition U V rather than incorrectly asserting that the interiors of A and B cover X.

Define the ordinary Mayer–Vietoris sequence on the homology of A ∩ B, A, B, and X, with the signed intersection map and addition map induced by the actual inclusions. The main result Hatcher.MayerVietoris.neighborhoodSequence_exact proves every adjacent six-term window exact; include the degree-zero epimorphism as a supporting theorem.

Transport the open-cover sequence for U,V across the three homology isomorphisms. Prove that the transported first and second maps are Hatcher's inclusion-induced maps, not merely unspecified conjugates. The connecting map may be defined by this transport. Since StrongDeformationRetract.toHomotopyEquiv points from a neighborhood to its retract, construct each inclusion-induced homology isomorphism from sdr.toHomotopyEquiv.symm.

This node uses the neutral Hatcher.StrongDeformationRetract interface, whose existing declaration now has a dedicated background roadmap article.

Sources

• Hatcher §2.2, neighborhood-deformation-retract extension, page 150
• Sphere-homology implementation specification

Dependencies

Statement usesTheorem 101 (The binary-cover Mayer–Vietoris sequence) · Theorem 50 (The standard cover of a well-pointed wedge) · Structure 4 (Strong deformation retracts)

Proof usesDefinition 77 (A homotopy equivalence induces homology isomorphisms)

Used byDefinition 109 (A closed ball strongly deformation retracts from Euclidean space) · Definition 107 (A sphere strongly deformation retracts from punctured Euclidean space) · Theorem 105 (The reduced neighborhood-retract Mayer–Vietoris sequence) · Definition 110 (The hemispheres have compatible neighborhood deformation retractions)

Theorem105The reduced neighborhood-retract Mayer–Vietoris sequence#✓fully proved

Let C be an abelian category with the coproducts required by the completed Mayer–Vietoris API, and let R : C. For Hatcher.MayerVietoris.NeighborhoodCover A B, define the reduced sequence on H̃_*(A ∩ B;R), H̃_*(A;R), H̃_*(B;R), and H̃_*(X;R). Its intersection and union maps are induced by the actual subspace inclusions with the same signs as the binary-cover sequence.

The main theorem Hatcher.MayerVietoris.reducedNeighborhoodLongExact packages exactness of every adjacent-degree window and, when A ∩ B is nonempty, the terminal exact sequence ending in H̃_0(X;R) ⟶ 0. Supporting naturality lemmas must identify the transported maps with the public reduced intersection and union maps. This node owns public formulas expressing the existing reducedIntersectionMap as the signed biproduct lift and reducedUnionMap as biprod.desc of the two inclusion-induced maps; the current private augmented-chain definitions are not an adequate downstream API by themselves.

Sources

• Hatcher §2.2, neighborhood-deformation-retract extension, page 150
• Sphere-homology implementation specification

Dependencies

Statement usesTheorem 102 (The ordinary neighborhood-retract Mayer–Vietoris sequence) · Theorem 104 (The reduced binary-cover Mayer–Vietoris sequence)

Proof usesDefinition 85 (A homotopy equivalence induces reduced-homology isomorphisms)

Used byTheorem 106 (The reduced homology of spheres satisfies the suspension recurrence)

Hemisphere geometry

Definition109A closed ball strongly deformation retracts from Euclidean space#✓fully proved

Let E be a real normed vector space and let r > 0. Construct the radial clamping retraction from E onto Metric.closedBall (0 : E) r, together with a homotopy from the identity to inclusion after retraction that fixes every point of the closed ball.

The main artifact is Hatcher.Sphere.closedBallStrongDeformationRetract, expressed using Hatcher.StrongDeformationRetract for the canonical subtype inclusion. It is the reusable Euclidean witness needed to transport a hemisphere from its punctured-sphere neighborhood.

Sources

• Hatcher §2.2, target hemisphere decomposition in Example 2.46
• Sphere-homology implementation specification

Dependencies

Statement usesTheorem 102 (The ordinary neighborhood-retract Mayer–Vietoris sequence)

Used byDefinition 110 (The hemispheres have compatible neighborhood deformation retractions)

Definition107A sphere strongly deformation retracts from punctured Euclidean space#✓fully proved

Let E be a nontrivial real normed vector space and let r > 0. Construct the normalization retraction from ({0}ᶜ : Set E) onto Metric.sphere (0 : E) r, and a radial homotopy from the identity to inclusion after retraction that fixes the radius-r sphere.

The main artifact is Hatcher.Sphere.spherePuncturedStrongDeformationRetract, expressed using the canonical subtype inclusion. Mathlib's homeomorphSphereProd is useful prior art, but the completion criterion is the strong deformation retraction needed by the neighborhood Mayer–Vietoris data.

Sources

• Hatcher §2.2, target equatorial decomposition in Example 2.46
• Sphere-homology implementation specification

Dependencies

Statement usesTheorem 102 (The ordinary neighborhood-retract Mayer–Vietoris sequence)

Used byTheorem 109 (Local homology of positive-dimensional Euclidean space) · Definition 110 (The hemispheres have compatible neighborhood deformation retractions)

Definition91Stereographic models for hemispheres and the equator#✓fully proved

For TopCat.sphere (n + 1), define the closed northern hemisphere, closed southern hemisphere, equator, north and south poles, and the two neighborhoods obtained by deleting the opposite poles. Bridge Mathlib's ULift-based TopCat.sphere once to the corresponding unit Metric.sphere so all public objects remain universe-polymorphic.

The main artifact Hatcher.Sphere.hemisphereChartData n packages the last-coordinate hemispheres, the poles ±e_last, and the neighborhoods given by their opposite-pole complements. Its stereographic homeomorphisms identify a hemisphere inside its neighborhood with Metric.closedBall 0 2 inside Euclidean space and the equator inside the overlap with Metric.sphere 0 2 inside punctured Euclidean space. It also records that the two hemispheres cover the sphere, their intersection is the equator, and the equator is homeomorphic to TopCat.sphere n. Include the commuting inclusion squares needed to transport strong deformation retractions back through these charts.

Sources

• Hatcher §2.2, Example 2.46, page 150
• Sphere-homology implementation specification

Dependencies

Used byDefinition 92 (A punctured sphere is Euclidean space) · Definition 110 (The hemispheres have compatible neighborhood deformation retractions) · Theorem 106 (The reduced homology of spheres satisfies the suspension recurrence)

Definition110The hemispheres have compatible neighborhood deformation retractions#✓fully proved

For every n, equip the northern and southern hemispheres of TopCat.sphere (n + 1) with the punctured-pole neighborhoods from the stereographic model. Transport the radial deformation retractions through the charts to obtain strong deformation retractions of each neighborhood onto its hemisphere and of their intersection onto the equator.

The main artifact Hatcher.Sphere.hemisphereNeighborhoodCover n is a Hatcher.MayerVietoris.NeighborhoodCover for the two closed hemispheres. It also exposes a nonempty point of the equator, needed by the terminal reduced sequence. The package must use the literal closed hemispheres of Example 2.46; it must not replace them silently by an antipodal-complement open cover.

Sources

• Hatcher §2.2, Example 2.46, page 150
• Sphere-homology implementation specification

Dependencies

Statement usesTheorem 102 (The ordinary neighborhood-retract Mayer–Vietoris sequence) · Definition 91 (Stereographic models for hemispheres and the equator)

Proof usesDefinition 109 (A closed ball strongly deformation retracts from Euclidean space) · Definition 107 (A sphere strongly deformation retracts from punctured Euclidean space)

Used byTheorem 106 (The reduced homology of spheres satisfies the suspension recurrence)

Sphere calculation

Theorem106The reduced homology of spheres satisfies the suspension recurrence#✓fully proved

Let C be an abelian category with HasCoproducts.{w} C, and let R : C. For a sphere dimension n, the main packaged theorem Hatcher.Sphere.reducedHomology_sphereSucc R n has the completion criterion

(∀ i, Nonempty (H̃_{i+1}(TopCat.sphere (n+1);R) ≅ H̃_i(TopCat.sphere n;R))) ∧ IsZero (H̃_0(TopCat.sphere (n+1);R)).

It keeps n and i separate and uses successor indices rather than truncated subtraction.

Apply the reduced neighborhood Mayer–Vietoris sequence to the two hemispheres. Contractibility makes the two middle summands zero, so exactness makes the connecting morphism both mono and epi and hence an isomorphism. Use the equator homeomorphism to identify the source-facing target with TopCat.sphere n.

Sources

• Hatcher §2.2, Example 2.46, page 150
• Sphere-homology implementation specification

Dependencies

Statement usesDefinition 65 (Reduced singular homology)

Proof usesTheorem 75 (Reduced homology of a contractible space vanishes) · Theorem 105 (The reduced neighborhood-retract Mayer–Vietoris sequence) · Definition 91 (Stereographic models for hemispheres and the equator) · Definition 110 (The hemispheres have compatible neighborhood deformation retractions)

Used byTheorem 108 (Reduced homology of spheres)

Definition111The zero-sphere is a two-point space#✓fully proved

Construct the explicit universe-polymorphic isomorphism

Hatcher.Sphere.zeroSphereIsoTwoPoint : TopCat.sphere (u := w) 0 ≅ TopCat.of (ULift.{w} Bool).

The two points must be distinguished explicitly and the isomorphism should make the induced map on path components usable by the degree-zero homology calculation. This node only identifies the topological model; it does not compute homology.

Sources

• Hatcher §2.1, Propositions 2.7–2.8 and the S⁰ base case in Corollary 2.14
• Sphere-homology implementation specification

Dependencies

Used byTheorem 107 (Reduced homology of the zero-sphere)

Theorem107Reduced homology of the zero-sphere#✓fully proved

Let C be an abelian category with HasCoproducts.{w} C, and let R : C. The main theorem Hatcher.Sphere.reducedHomology_sphere_zero R has the completion criterion

Nonempty (H̃_0(TopCat.sphere 0;R) ≅ R) ∧ ∀ i, i ≠ 0 → IsZero (H̃_i(TopCat.sphere 0;R)).

Use the two path components of S⁰ to identify ordinary zeroth homology with R ⊞ R, including the explicit comparison ∐ (_ : ULift Bool), R ≅ R ⊞ R. Prove that defined reduced zeroth homology is the kernel of the induced ordinary-H₀ augmentation, identify that map with the codiagonal, and compute its kernel as the antidiagonal copy of R. Do not use cancellation of biproduct summands in an arbitrary abelian category. Positive-degree vanishing follows from the totally-disconnected calculation and the reduced/ordinary comparison.

Sources

• Hatcher §2.1, Propositions 2.7–2.8 and Corollary 2.14, pages 109–114
• Sphere-homology implementation specification

Dependencies

Statement usesDefinition 65 (Reduced singular homology)

Proof usesDefinition 111 (The zero-sphere is a two-point space) · Definition 73 (Zeroth homology is free on path components) · Definition 72 (Zeroth homology splits into reduced homology and the coefficient object) · Lemma 5 (Higher homology vanishes for totally disconnected spaces) · Definition 71 (Reduced and ordinary homology agree in positive degrees)

Used byTheorem 108 (Reduced homology of spheres)

Theorem108Reduced homology of spheres#✓fully proved

Let C be an abelian category with HasCoproducts.{w} C, and let R : C. For every sphere dimension n, the main theorem Hatcher.Sphere.reducedHomology_sphere R n has the completion criterion

Nonempty (H̃_n(TopCat.sphere n;R) ≅ R) ∧ ∀ i, i ≠ n → IsZero (H̃_i(TopCat.sphere n;R)).

Induct on the sphere dimension using the successor recurrence and the direct S⁰ calculation. Return the diagonal isomorphism under Nonempty rather than choosing an orientation. Include Hatcher.Sphere.reducedHomology_sphere_int as the explicit specialization to AddCommGrpCat.of ℤ matching Hatcher's Corollary 2.14.

Sources

• Hatcher §2.1, Corollary 2.14, page 114
• Hatcher §2.2, alternative proof in Example 2.46, page 150
• Sphere-homology implementation specification

Dependencies

Statement usesDefinition 65 (Reduced singular homology)

Proof usesTheorem 106 (The reduced homology of spheres satisfies the suspension recurrence) · Theorem 107 (Reduced homology of the zero-sphere)

Used byTheorem 109 (Local homology of positive-dimensional Euclidean space) · Theorem 113 (The boundary sphere is not a retract of the disk)

Corollary 2.15

Theorem113The boundary sphere is not a retract of the disk#✓fully proved

For every n : ℕ, there is no morphism

r : TopCat.disk.{0} (n + 1) ⟶ TopCat.diskBoundary.{0} (n + 1)

such that

TopCat.diskBoundaryInclusion.{0} (n + 1) ≫ r = 𝟙 _.

The intended main result is Hatcher.Disc.not_exists_diskBoundary_retraction. Apply reduced integral homology in degree n. The boundary is TopCat.sphere.{0} n, with reduced homology isomorphic to ℤ, while the contractible disk has zero reduced homology. A retraction would make the identity of the former factor through the latter.

Sources

• Hatcher §2.1, Corollary 2.15, pages 114–115
• Corollary 2.15 implementation specification

Dependencies

Proof usesTheorem 75 (Reduced homology of a contractible space vanishes) · Theorem 108 (Reduced homology of spheres)

Used byTheorem 115 (Brouwer's fixed-point theorem for disks)

Theorem114A fixed-point-free disk map produces a boundary retraction#✓fully proved

For every n : ℕ, let

f : TopCat.disk.{0} (n + 1) ⟶ TopCat.disk.{0} (n + 1)

and assume

hf : ∀ x : TopCat.disk.{0} (n + 1), f x ≠ x.

Then construct a morphism

r : TopCat.disk.{0} (n + 1) ⟶ TopCat.diskBoundary.{0} (n + 1)

with TopCat.diskBoundaryInclusion.{0} (n + 1) ≫ r = 𝟙 _.

The intended main result is Hatcher.Disc.exists_diskBoundary_retraction_of_fixedPointFree. On the raw closed ball, send x to the point where the ray from f(x) through x exits the ball. The fixed-point-free hypothesis makes the ray nondegenerate; continuity of its exit parameter and the boundary formula show that this map is a retraction. Transport the construction through Mathlib's ULift disk model.

Sources

• Hatcher §1.1, proof of Theorem 1.9, pages 31–32
• Hatcher §2.1, Corollary 2.15, pages 114–115
• Corollary 2.15 implementation specification

Dependencies

Used byTheorem 115 (Brouwer's fixed-point theorem for disks)

Theorem115Brouwer's fixed-point theorem for disks#✓fully proved

For every n : ℕ and every morphism

f : TopCat.disk.{0} (n + 1) ⟶ TopCat.disk.{0} (n + 1),

there is a point x with f x = x.

The intended main result is Hatcher.Disc.exists_fixed_point_disk. If f had no fixed point, the boundary-ray construction would give a retraction of the disk onto its boundary, contradicting the homological no-retraction theorem.

Sources

• Hatcher §2.1, Corollary 2.15, pages 114–115
• Hatcher §1.1, proof of Theorem 1.9, pages 31–32
• Corollary 2.15 implementation specification

Dependencies

Proof usesTheorem 113 (The boundary sphere is not a retract of the disk) · Theorem 114 (A fixed-point-free disk map produces a boundary retraction)

Boundary

This milestone assumes the neighborhoods and deformation retractions in the general transport theorem, and constructs only the sphere-specific witnesses needed for Example 2.46. It excludes Hatcher's general CW-subcomplex Nε(A) construction and does not use Theorem 2.13 or Proposition 2.22; those two results are decomposed separately in the good-pair quotient milestone. It also excludes degree and orientation theory, invariance of dimension, cellular homology, Examples 2.47–2.48, mapping tori, relative Mayer–Vietoris, and coefficients as a separate source topic.

Sources

• Hatcher §2.1 source note
• Hatcher §2.2 source note
• Sphere-homology implementation specification
• Corollary 2.15 implementation specification