Ball--boundary long-exact-sequence route for sphere homology

Develops the contractibility and positive-degree homology vanishing of the disk and records the relative-homology input needed by the classical pair (Dⁿ⁺¹, Sⁿ) argument. This is an alternate route; the unconditional sphere top-homology theorem used by the public API is obtained through the Mayer--Vietoris suspension construction.

Homology isomorphism from a homotopy equivalence of spaces

noncomputable def SphereOddDegree.singularHomologyℤIsoOfHomotopyEquivSpace (k : ℕ) {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (e : ContinuousMap.HomotopyEquiv X Y) : (singularHomologyℤ k).obj ↧X ≅ (singularHomologyℤ k).obj ↧Y

Homology iso from a homotopy equivalence. A homotopy equivalence e : X ≃ₕ Y of topological spaces induces an isomorphism on the k-th integral singular homology, by the library's unconditional homotopy invariance. The two maps are the homologies of e.toFun and e.invFun; the round-trip identities hold because e.invFun ∘ e.toFun (resp. e.toFun ∘ e.invFun) is homotopic to the identity.

Equations

• One or more equations did not get rendered due to their size.

Contractible spaces have vanishing positive homology

theorem SphereOddDegree.isZero_singularHomologyℤ_of_contractibleSpace (k : ℕ) (hk : 1 ≤ k) (X : Type) [TopologicalSpace X] [ContractibleSpace X] : CategoryTheory.Limits.IsZero ((singularHomologyℤ k).obj ↧X)

Vanishing of positive homology for contractible spaces. If X is contractible and k ≥ 1, then Hₖ(X; ℤ) = 0. Indeed X is homotopy equivalent to a point (ContractibleSpace.hequiv_unit), and the higher homology of a point vanishes (it is totally disconnected).

The disk Dⁿ⁺¹ and its vanishing homology

@[reducible, inline]

abbrev SphereOddDegree.Disk (n : ℕ) : Type

A concrete model of the closed disk Dⁿ⁺¹ as the closed unit ball in EuclideanSpace ℝ (Fin (n+1)). Its topological boundary is the library's Sphere n.

Equations

• SphereOddDegree.Disk n = ↑(Metric.closedBall 0 1)

instance SphereOddDegree.instContractibleSpaceDisk (n : ℕ) : ContractibleSpace (Disk n)

The disk Dⁿ⁺¹ is contractible: it is a nonempty convex set.

theorem SphereOddDegree.isZero_singularHomologyℤ_disk (k n : ℕ) (hk : 1 ≤ k) : CategoryTheory.Limits.IsZero ((singularHomologyℤ k).obj ↧(Disk n))

Homology of the disk. For k ≥ 1, Hₖ(Dⁿ⁺¹; ℤ) = 0, since the disk is contractible.