The Mayer–Vietoris recursive step for sphere homology

For n ≥ 1 we prove Hₙ₊₁(Sⁿ⁺¹; ℤ) ≅ Hₙ(Sⁿ; ℤ) (sphereTopHomologyStepMV), the recursive step of SphereSuspensionTower.

Cover Sⁿ⁺¹ by the two punctured spheres U = Sⁿ⁺¹ \ {north} and V = Sⁿ⁺¹ \ {south}. Both are contractible (stereographic projection), so their positive homology vanishes, and the Mayer–Vietoris connecting isomorphism (mvHomologyIsoSucc) gives Hₙ₊₁(Sⁿ⁺¹) ≅ Hₙ(U ∩ V). The intersection U ∩ V is the equatorial band, homotopy equivalent to Sⁿ; the subspace bridge (subspaceHomologyIsoℤ) and homotopy invariance then identify its homology with Hₙ(Sⁿ).

def SphereOddDegree.northVec (n : ℕ) : EuclideanSpace ℝ (Fin (n + 2))

The north pole of Sⁿ⁺¹ as a unit vector e₀.

Equations

• SphereOddDegree.northVec n = PiLp.single 2 0 1

theorem SphereOddDegree.norm_northVec (n : ℕ) : ‖northVec n‖ = 1

def SphereOddDegree.northPole (n : ℕ) : Sphere (n + 1)

The north pole of Sⁿ⁺¹.

Equations

• SphereOddDegree.northPole n = ⟨SphereOddDegree.northVec n, ⋯⟩

def SphereOddDegree.southPole (n : ℕ) : Sphere (n + 1)

The south pole of Sⁿ⁺¹, the antipode of the north pole.

Equations

• SphereOddDegree.southPole n = ⟨-SphereOddDegree.northVec n, ⋯⟩

theorem SphereOddDegree.northPole_ne_southPole (n : ℕ) : northPole n ≠ southPole n

def SphereOddDegree.upperPunctured (n : ℕ) : Set (Sphere (n + 1))

The upper punctured sphere Sⁿ⁺¹ \ {north}.

Equations

• SphereOddDegree.upperPunctured n = {SphereOddDegree.northPole n}ᶜ

def SphereOddDegree.lowerPunctured (n : ℕ) : Set (Sphere (n + 1))

The lower punctured sphere Sⁿ⁺¹ \ {south}.

Equations

• SphereOddDegree.lowerPunctured n = {SphereOddDegree.southPole n}ᶜ

theorem SphereOddDegree.isOpen_upperPunctured (n : ℕ) : IsOpen (upperPunctured n)

theorem SphereOddDegree.isOpen_lowerPunctured (n : ℕ) : IsOpen (lowerPunctured n)

theorem SphereOddDegree.upper_union_lower (n : ℕ) : upperPunctured n ∪ lowerPunctured n = Set.univ

def SphereOddDegree.sphereBand (n : ℕ) : Set (Sphere (n + 1))

The equatorial band Sⁿ⁺¹ \ {north, south}.

Equations

• SphereOddDegree.sphereBand n = SphereOddDegree.upperPunctured n ∩ SphereOddDegree.lowerPunctured n

Contractibility of the punctured spheres

instance SphereOddDegree.contractible_upperPunctured (n : ℕ) : ContractibleSpace ↑(upperPunctured n)

instance SphereOddDegree.contractible_lowerPunctured (n : ℕ) : ContractibleSpace ↑(lowerPunctured n)

The equatorial band is homotopy equivalent to Sⁿ

Construction of the band ≃ Sⁿ homotopy equivalence

def SphereOddDegree.eqNormSq (n : ℕ) (x : Sphere (n + 1)) : ℝ

The squared norm of the equatorial part (coordinates 1 .. n+1) of a point of Sⁿ⁺¹.

Equations

• SphereOddDegree.eqNormSq n x = ∑ i : Fin (n + 1), (↑x).ofLp i.succ ^ 2

theorem SphereOddDegree.eqNormSq_eq (n : ℕ) (x : Sphere (n + 1)) : eqNormSq n x = 1 - (↑x).ofLp 0 ^ 2

theorem SphereOddDegree.eqNormSq_pos (n : ℕ) {x : Sphere (n + 1)} (hx : x ∈ sphereBand n) : 0 < eqNormSq n x

noncomputable def SphereOddDegree.fFun (n : ℕ) (x : Sphere (n + 1)) : EuclideanSpace ℝ (Fin (n + 1))

The equatorial-projection map underlying band → Sⁿ: drop coordinate 0 and normalize.

Equations

• SphereOddDegree.fFun n x = (WithLp.equiv 2 (Fin (n + 1) → ℝ)).symm fun (i : Fin (n + 1)) => (↑x).ofLp i.succ / √(SphereOddDegree.eqNormSq n x)

theorem SphereOddDegree.fFun_mem (n : ℕ) {x : Sphere (n + 1)} (hx : x ∈ sphereBand n) : fFun n x ∈ Metric.sphere 0 1

theorem SphereOddDegree.continuous_fFun_band (n : ℕ) : Continuous fun (x : ↑(sphereBand n)) => ⟨fFun n ↑x, ⋯⟩

noncomputable def SphereOddDegree.bandToSphere (n : ℕ) : C(↑(sphereBand n), Sphere n)

The continuous map band → Sⁿ.

Equations

• SphereOddDegree.bandToSphere n = { toFun := fun (x : ↑(SphereOddDegree.sphereBand n)) => ⟨SphereOddDegree.fFun n ↑x, ⋯⟩, continuous_toFun := ⋯ }

def SphereOddDegree.gFun (n : ℕ) (y : Sphere n) : EuclideanSpace ℝ (Fin (n + 2))

The inclusion map underlying Sⁿ → band: prepend a 0 coordinate.

Equations

• SphereOddDegree.gFun n y = (WithLp.equiv 2 (Fin (n + 2) → ℝ)).symm (Fin.cons 0 fun (i : Fin (n + 1)) => (↑y).ofLp i)

theorem SphereOddDegree.gFun_mem_sphere (n : ℕ) (y : Sphere n) : gFun n y ∈ Metric.sphere 0 1

theorem SphereOddDegree.gFun_mem_band (n : ℕ) (y : Sphere n) : ⟨gFun n y, ⋯⟩ ∈ sphereBand n

theorem SphereOddDegree.continuous_gFun (n : ℕ) : Continuous fun (y : Sphere n) => ⟨⟨gFun n y, ⋯⟩, ⋯⟩

def SphereOddDegree.sphereToBand (n : ℕ) : C(Sphere n, ↑(sphereBand n))

The continuous map Sⁿ → band.

Equations

• SphereOddDegree.sphereToBand n = { toFun := fun (y : SphereOddDegree.Sphere n) => ⟨⟨SphereOddDegree.gFun n y, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }

theorem SphereOddDegree.bandToSphere_comp_sphereToBand (n : ℕ) : (bandToSphere n).comp (sphereToBand n) = ContinuousMap.id (Sphere n)

noncomputable def SphereOddDegree.bandHomotopyFun (n : ℕ) (p : ↑unitInterval × ↑(sphereBand n)) : EuclideanSpace ℝ (Fin (n + 2))

The straight-line-on-the-sphere homotopy from sphereToBand ∘ bandToSphere to the identity of the band.

Equations

• SphereOddDegree.bandHomotopyFun n p = (1 - ↑p.1) • ↑↑((SphereOddDegree.sphereToBand n) ((SphereOddDegree.bandToSphere n) p.2)) + ↑p.1 • ↑↑p.2

theorem SphereOddDegree.bandHomotopyFun_ne_zero (n : ℕ) (p : ↑unitInterval × ↑(sphereBand n)) : bandHomotopyFun n p ≠ 0

theorem SphereOddDegree.bandHomotopy_mem_sphere (n : ℕ) (p : ↑unitInterval × ↑(sphereBand n)) : ‖bandHomotopyFun n p‖⁻¹ • bandHomotopyFun n p ∈ Metric.sphere 0 1

theorem SphereOddDegree.bandHomotopy_mem_band (n : ℕ) (p : ↑unitInterval × ↑(sphereBand n)) : ⟨‖bandHomotopyFun n p‖⁻¹ • bandHomotopyFun n p, ⋯⟩ ∈ sphereBand n

theorem SphereOddDegree.continuous_bandHomotopy (n : ℕ) : Continuous fun (p : ↑unitInterval × ↑(sphereBand n)) => ⟨⟨‖bandHomotopyFun n p‖⁻¹ • bandHomotopyFun n p, ⋯⟩, ⋯⟩

theorem SphereOddDegree.bandHomotopy_zero (n : ℕ) (x : ↑(sphereBand n)) : ⟨⟨‖bandHomotopyFun n (0, x)‖⁻¹ • bandHomotopyFun n (0, x), ⋯⟩, ⋯⟩ = ((sphereToBand n).comp (bandToSphere n)) x

theorem SphereOddDegree.bandHomotopy_one (n : ℕ) (x : ↑(sphereBand n)) : ⟨⟨‖bandHomotopyFun n (1, x)‖⁻¹ • bandHomotopyFun n (1, x), ⋯⟩, ⋯⟩ = (ContinuousMap.id ↑(sphereBand n)) x

noncomputable def SphereOddDegree.bandHomotopy (n : ℕ) : ((sphereToBand n).comp (bandToSphere n)).Homotopy (ContinuousMap.id ↑(sphereBand n))

The homotopy sphereToBand ∘ bandToSphere ≃ id.

Equations

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

noncomputable def SphereOddDegree.sphereBandHomotopyEquiv (n : ℕ) : ContinuousMap.HomotopyEquiv (↑(sphereBand n)) (Sphere n)

The equatorial band Sⁿ⁺¹ \ {north, south} is homotopy equivalent to Sⁿ.

Equations

• SphereOddDegree.sphereBandHomotopyEquiv n = { toFun := SphereOddDegree.bandToSphere n, invFun := SphereOddDegree.sphereToBand n, left_inv := ⋯, right_inv := ⋯ }

Assembly of the Mayer–Vietoris step

@[reducible, inline]

abbrev SphereOddDegree.sphereSpace (n : ℕ) : TopCat

The categorical space Sⁿ⁺¹ realized as a TopCat from the library model.

Equations

• SphereOddDegree.sphereSpace n = ↧(SphereOddDegree.Sphere (n + 1))

def SphereOddDegree.upperOpens (n : ℕ) : TopologicalSpace.Opens ↑(sphereSpace n)

The upper punctured sphere as an open set of Sⁿ⁺¹.

Equations

• SphereOddDegree.upperOpens n = { carrier := SphereOddDegree.upperPunctured n, is_open' := ⋯ }

def SphereOddDegree.lowerOpens (n : ℕ) : TopologicalSpace.Opens ↑(sphereSpace n)

The lower punctured sphere as an open set of Sⁿ⁺¹.

Equations

• SphereOddDegree.lowerOpens n = { carrier := SphereOddDegree.lowerPunctured n, is_open' := ⋯ }

instance SphereOddDegree.contractible_upperOpens (n : ℕ) : ContractibleSpace ↑↑(upperOpens n)

instance SphereOddDegree.contractible_lowerOpens (n : ℕ) : ContractibleSpace ↑↑(lowerOpens n)

theorem SphereOddDegree.upperOpens_sup_lowerOpens (n : ℕ) : upperOpens n ⊔ lowerOpens n = ⊤

noncomputable def SphereOddDegree.bandHomologyIso (n : ℕ) : HomologicalComplex.homology (subChainComplex ℤ (sphereSpace n) (↑(upperOpens n) ∩ ↑(lowerOpens n))) n ≅ sphereTopHomologyℤ n

The integral homology of the band is isomorphic to Hₙ(Sⁿ; ℤ), via the subspace bridge and homotopy invariance.

Equations

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

noncomputable def SphereOddDegree.sphereTopHomologyStepMV (n : ℕ) (hn : 1 ≤ n) : sphereTopHomologyℤ (n + 1) ≅ sphereTopHomologyℤ n

The Mayer–Vietoris recursive step. For n ≥ 1, Hₙ₊₁(Sⁿ⁺¹; ℤ) ≅ Hₙ(Sⁿ; ℤ).

Equations

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