Sphere top homology from a suspension tower

Defines SphereSuspensionTower and derives Hₙ(Sⁿ; ℤ) ≅ ℤ for every n ≥ 1 by induction. The n = 0 obstruction is recorded explicitly because S⁰ has two connected components. A concrete suspension tower and the resulting unconditional orientation are constructed in the Mayer--Vietoris sphere-homology modules.

Suspension tower for sphere top homology

structure SphereOddDegree.SphereSuspensionTower : Type

A suspension tower for the integral top homology of spheres.

It bundles exactly the classical inductive data computing Hₙ(Sⁿ; ℤ):

• base : H₁(S¹; ℤ) ≅ ℤ, the degenerate first instance, and
• step n (h : 1 ≤ n) : Hₙ₊₁(Sⁿ⁺¹; ℤ) ≅ Hₙ(Sⁿ; ℤ), the top-degree suspension isomorphism.

A term of this structure is equivalent to the required suspension theorem for singular homology; from it the whole family SphereTopHomologyIso n (n ≥ 1) follows by induction.

• base : SphereTopHomologyIso 1

  The base identification H₁(S¹; ℤ) ≅ ℤ.

• step (n : ℕ) : 1 ≤ n → (sphereTopHomologyℤ (n + 1) ≅ sphereTopHomologyℤ n)

  The top-degree suspension isomorphism Hₙ₊₁(Sⁿ⁺¹; ℤ) ≅ Hₙ(Sⁿ; ℤ), for every n ≥ 1.

noncomputable def SphereOddDegree.SphereSuspensionTower.isoSucc (T : SphereSuspensionTower) (k : ℕ) : SphereTopHomologyIso (k + 1)

The shifted top-homology identification Hₖ₊₁(Sᵏ⁺¹; ℤ) ≅ ℤ, defined by structural recursion on k: the base case k = 0 is T.base, and each successor composes the suspension isomorphism T.step with the identification one dimension lower. (Nat.le_induction only eliminates into Prop, so the data-valued family is built on the shifted index instead.)

Equations

• T.isoSucc k = Nat.rec T.base (fun (j : ℕ) (ih : SphereOddDegree.SphereTopHomologyIso (j + 1)) => T.step (j + 1) ⋯ ≪≫ ih) k

noncomputable def SphereOddDegree.SphereSuspensionTower.iso (T : SphereSuspensionTower) (n : ℕ) : 1 ≤ n → SphereTopHomologyIso n

From a suspension tower, the top-homology identification Hₙ(Sⁿ; ℤ) ≅ ℤ for every n ≥ 1.

Equations

• T.iso k.succ x_2 = T.isoSucc k

@[simp]

theorem SphereOddDegree.SphereSuspensionTower.isoSucc_zero (T : SphereSuspensionTower) : T.isoSucc 0 = T.base

A non-vacuous positive orientation (dimensions n ≥ 1)

structure SphereOddDegree.SphereOrientationPos : Type

A positive sphere orientation: a choice of top-homology identification Hₙ(Sⁿ; ℤ) ≅ ℤ in every dimension n ≥ 1.

Unlike SphereOrientation (whose ∀ n field is uninhabited because it demands the false n = 0 case H₀(S⁰; ℤ) ≅ ℤ), this structure restricts to the dimensions n ≥ 1 where the integral top-homology degree theory lives, and is genuinely inhabited as soon as a SphereSuspensionTower is available.

• iso (n : ℕ) : 1 ≤ n → SphereTopHomologyIso n

  The identification Hₙ(Sⁿ; ℤ) ≅ ℤ in each dimension n ≥ 1.

noncomputable def SphereOddDegree.SphereOrientationPos.degree (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : ℤ

The integer degree of a self-map of Sphere n (n ≥ 1), read off the supplied top-homology identification o.iso n hn. Honest and unconditional once a SphereOrientationPos is provided.

Equations

• o.degree hn f = SphereOddDegree.degreeOfIso (o.iso n hn) f

@[simp]

theorem SphereOddDegree.SphereOrientationPos.degree_id (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) : o.degree hn (ContinuousMap.id (Sphere n)) = 1

The degree of the identity map is 1.

theorem SphereOddDegree.SphereOrientationPos.degree_comp (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (f g : C(Sphere n, Sphere n)) : o.degree hn (g.comp f) = o.degree hn g * o.degree hn f

The degree is multiplicative: degree (g ∘ f) = degree g * degree f.

theorem SphereOddDegree.SphereOrientationPos.degree_well_defined (o o' : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : o.degree hn f = o'.degree hn f

Choice independence. Any two positive orientations assign the same degree.

theorem SphereOddDegree.SphereOrientationPos.degree_eq_of_homotopic (o : SphereOrientationPos) (prism : SingularPrismOperator) {n : ℕ} (hn : 1 ≤ n) {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) : o.degree hn f = o.degree hn g

Homotopy invariance of the degree (conditional on the prism operator). Homotopic self-maps of Sphere n (n ≥ 1) have equal degree.

noncomputable def SphereOddDegree.SphereSuspensionTower.orientation (T : SphereSuspensionTower) : SphereOrientationPos

A suspension tower yields a genuine (non-vacuous) positive orientation.

Equations

• T.orientation = { iso := T.iso }

@[simp]

theorem SphereOddDegree.SphereSuspensionTower.orientation_iso (T : SphereSuspensionTower) (n : ℕ) (hn : 1 ≤ n) : T.orientation.iso n hn = T.iso n hn

The n = 0 obstruction, proved

The n = 0 case is a genuine obstruction: H₀(S⁰; ℤ) ≅ ℤ², so there is no identification H₀(S⁰; ℤ) ≅ ℤ. Consequently the structural SphereOrientation of SphereTopHomology.lean (whose field demands a term of SphereTopHomologyIso n for every n, including n = 0) is uninhabited — which is exactly why the non-vacuous SphereOrientationPos (restricted to n ≥ 1) is the correct structure.

noncomputable def SphereOddDegree.sphere0H0IsoCoprod : sphereTopHomologyℤ 0 ≅ ∐ fun (x : ↑(TopCat.sphere 0)) => ↧ℤ

H₀(S⁰; ℤ) is the categorical coproduct of one copy of ℤ per point of the two-point space S⁰, via Mathlib's totally-disconnected computation.

Equations

• SphereOddDegree.sphere0H0IsoCoprod = AlgebraicTopology.singularHomologyFunctorZeroOfTotallyDisconnectedSpace (ModuleCat ℤ) (↧ℤ) (TopCat.sphere 0)

theorem SphereOddDegree.card_topCatSphere_zero : Nat.card ↑(TopCat.sphere 0) = 2

theorem SphereOddDegree.finrank_sphereTopHomologyℤ_zero : Module.finrank ℤ ↑(sphereTopHomologyℤ 0) = 2

theorem SphereOddDegree.sphereTopHomologyIso_zero_isEmpty : IsEmpty (SphereTopHomologyIso 0)

The n = 0 obstruction is genuine. There is no identification H₀(S⁰; ℤ) ≅ ℤ: H₀(S⁰; ℤ) has ℤ-rank 2 (finrank_sphereTopHomologyℤ_zero), whereas ℤ has rank 1.

theorem SphereOddDegree.sphereOrientation_isEmpty : IsEmpty SphereOrientation

The structural SphereOrientation is uninhabited, because it demands the impossible n = 0 identification H₀(S⁰; ℤ) ≅ ℤ. (The correct non-vacuous structure is SphereOrientationPos, which only requires n ≥ 1.)