Reduced-to-unreduced bridge for sphere top homology

This file builds the genuine reduced-to-unreduced comparison for integral singular homology and uses it to reduce the positive-dimensional sphere top-homology family to the corresponding reduced statement.

Reduced homology, honestly

Pinned Mathlib (v4.28.0, commit 8f9d9cff6bd728b17a24e163c9402775d9e6a365) has no reduced-homology API, no suspension, no Mayer–Vietoris and no excision (see than assume a reduced theory, we define reduced integral singular homology in the standard way, as the kernel of the augmentation to a point:

H_tildeₙ(X; ℤ) := ker ( Hₙ(X; ℤ) --Hₙ(X → pt)--> Hₙ(pt; ℤ) ).

This is a legitimate definition of reduced homology (the kernel of the map induced by the unique map to a one-point space), and it requires

The bridge (proved)

For n ≥ 1 the point has vanishing homology Hₙ(pt; ℤ) = 0 (the one-point space is totally disconnected, via Mathlib's isZero_singularHomologyFunctor_of_totallyDisconnectedSpace). Hence the augmentation Hₙ(X) → Hₙ(pt) is the zero map and its kernel is all of Hₙ(X):

n ≥ 1 ⇒ H_tildeₙ(X; ℤ) ≅ Hₙ(X; ℤ). (`reducedToUnreducedIso`)

This is the exact reduced/unreduced comparison theorem requested by the project, proved as an actual Lean isomorphism, not assumed.

Consequence for the sphere top-homology family

Transporting along the bridge turns a reduced sphere top-homology computation into the ordinary one consumed by the degree API:

(∀ n ≥ 1, H_tildeₙ(Sⁿ; ℤ) ≅ ℤ) ⇒ ∀ n ≥ 1, Hₙ(Sⁿ; ℤ) ≅ ℤ.

i.e. sphereTopHomologyIsoPosOfReducedSphereHomology, and as a SphereOrientationPos via sphereOrientationPosOfReducedSphereHomology.

Honest blocker recorded

In the positive degree regime reduced and unreduced homology coincide (this file proves exactly that), so the bridge alone supplies no new computation: the hypothesis H_tildeₙ(Sⁿ) ≅ ℤ for n ≥ 1 is, via the bridge, equivalent to the goal Hₙ(Sⁿ) ≅ ℤ. The genuine content needed to discharge that reduced hypothesis is the reduced suspension isomorphism H_tildeₖ(Sⁿ) ≅ H_tildeₖ₋₁(Sⁿ⁻¹) (with base H_tilde₀(S⁰) ≅ ℤ), which rests on Mayer–Vietoris / excision and is absent from pinned Mathlib. Consequently SphereSuspensionTower.step is not fillable from this choice, Quot.sound`).

The one-point space and the augmentation map

def SphereOddDegree.toPUnit (X : TopCat) : X ⟶ ↧PUnit.{1}

The unique continuous map from a space X to the one-point space PUnit. It induces the augmentation on homology.

Equations

• SphereOddDegree.toPUnit X = TopCat.ofHom { toFun := fun (x : ↑X) => PUnit.unit, continuous_toFun := ⋯ }

noncomputable def SphereOddDegree.reducedSingularHomologyℤ (n : ℕ) (X : TopCat) : ModuleCat ℤ

Reduced integral singular homology of a space X, defined as the kernel of the augmentation Hₙ(X; ℤ) → Hₙ(pt; ℤ) induced by the unique map X → pt.

Equations

• SphereOddDegree.reducedSingularHomologyℤ n X = CategoryTheory.Limits.kernel ((SphereOddDegree.singularHomologyℤ n).map (SphereOddDegree.toPUnit X))

Vanishing of point homology in positive degree

theorem SphereOddDegree.isZero_singularHomologyℤ_punit_of_pos (n : ℕ) (hn : 1 ≤ n) : CategoryTheory.Limits.IsZero ((singularHomologyℤ n).obj ↧PUnit.{1})

Hₙ(pt; ℤ) = 0 for n ≥ 1: the one-point space is totally disconnected, so its higher singular homology vanishes.

The reduced-to-unreduced bridge

noncomputable def SphereOddDegree.reducedToUnreducedIsoOfIsZero (n : ℕ) (X : TopCat) (hpt : CategoryTheory.Limits.IsZero ((singularHomologyℤ n).obj ↧PUnit.{1})) : reducedSingularHomologyℤ n X ≅ (singularHomologyℤ n).obj X

Bridge, general form. Whenever the point's n-th homology vanishes, reduced and unreduced n-th homology of X agree. The augmentation Hₙ(X) → Hₙ(pt) is then the zero map, whose kernel is all of Hₙ(X).

Equations

• SphereOddDegree.reducedToUnreducedIsoOfIsZero n X hpt = CategoryTheory.Limits.kernelIsoOfEq ⋯ ≪≫ CategoryTheory.Limits.kernelZeroIsoSource

noncomputable def SphereOddDegree.reducedToUnreducedIso (n : ℕ) (hn : 1 ≤ n) (X : TopCat) : reducedSingularHomologyℤ n X ≅ (singularHomologyℤ n).obj X

Reduced-to-unreduced bridge. For n ≥ 1, reduced and unreduced integral singular homology agree: H_tildeₙ(X; ℤ) ≅ Hₙ(X; ℤ).

Equations

• SphereOddDegree.reducedToUnreducedIso n hn X = SphereOddDegree.reducedToUnreducedIsoOfIsZero n X ⋯

Consequence for the sphere top-homology family

noncomputable def SphereOddDegree.sphereTopHomologyIsoOfReduced {n : ℕ} (hn : 1 ≤ n) (e : reducedSingularHomologyℤ n (TopCat.sphere n) ≅ ↧ℤ) : SphereTopHomologyIso n

Transport a reduced sphere top-homology identification H_tildeₙ(Sⁿ; ℤ) ≅ ℤ (n ≥ 1) across the bridge to the ordinary identification Hₙ(Sⁿ; ℤ) ≅ ℤ required by the degree API.

Equations

• SphereOddDegree.sphereTopHomologyIsoOfReduced hn e = (SphereOddDegree.reducedToUnreducedIso n hn (TopCat.sphere n)).symm ≪≫ e

noncomputable def SphereOddDegree.sphereTopHomologyIsoPosOfReducedSphereHomology (red : (n : ℕ) → 1 ≤ n → (reducedSingularHomologyℤ n (TopCat.sphere n) ≅ ↧ℤ)) (n : ℕ) : 1 ≤ n → SphereTopHomologyIso n

Reduced ⇒ ordinary, for the whole positive family. A reduced sphere top-homology computation in every dimension n ≥ 1 yields the ordinary top-homology identification Hₙ(Sⁿ; ℤ) ≅ ℤ in every dimension n ≥ 1.

Equations

• SphereOddDegree.sphereTopHomologyIsoPosOfReducedSphereHomology red n hn = SphereOddDegree.sphereTopHomologyIsoOfReduced hn (red n hn)

noncomputable def SphereOddDegree.sphereOrientationPosOfReducedSphereHomology (red : (n : ℕ) → 1 ≤ n → (reducedSingularHomologyℤ n (TopCat.sphere n) ≅ ↧ℤ)) : SphereOrientationPos

A reduced sphere top-homology computation yields a genuine (non-vacuous) positive sphere orientation, hence the unconditional positive-degree theory.

Equations

• SphereOddDegree.sphereOrientationPosOfReducedSphereHomology red = { iso := SphereOddDegree.sphereTopHomologyIsoPosOfReducedSphereHomology red }