13.6. SphereTopology.SphereSimplyConnected🔗

Jacobians.SphereTopology.SphereSimplyConnected — source

TwoOpenVanKampen

Two-open van Kampen. A space that is path-connected and is the union of two open simply connected subsets with path-connected intersection is simply connected. This is the only piece of the SimplyConnectedSpace (OnePoint ℂ) proof that Mathlib does not supply (no Seifert–van Kampen for π₁); every *use* of it below has all side-conditions discharged.

def TwoOpenVanKampen : Prop

isSimplyConnected_compl_infty

The affine chart U = {∞}ᶜ is simply connected: it is range (↑) ≃ₜ ℂ, and ℂ is a real topological vector space, hence contractible, hence simply connected.

theorem isSimplyConnected_compl_infty :
    IsSimplyConnected ({∞}ᶜ : Set (OnePoint ℂ))

isSimplyConnected_compl_zero

The ∞-chart V = {0}ᶜ is simply connected: it is the image of the affine chart {∞}ᶜ under the inversion self-homeomorphism inversionHomeomorph (which swaps 0 ↔ ∞), so V = inversionHomeomorph '' {∞}ᶜ, and simple-connectivity is a homeomorphism invariant.

theorem isSimplyConnected_compl_zero :
    IsSimplyConnected ({((0 : ℂ) : OnePoint ℂ)}ᶜ : Set (OnePoint ℂ))

union_charts_eq_univ

The two charts cover the sphere: {∞}ᶜ ∪ {0}ᶜ = univ (no point is both ∞ and 0).

theorem union_charts_eq_univ :
    ({∞}ᶜ : Set (OnePoint ℂ)) ∪ ({((0 : ℂ) : OnePoint ℂ)}ᶜ) = Set.univ

isPathConnected_inter_charts

The overlap of the two charts is path-connected: {∞}ᶜ ∩ {0}ᶜ is the image under coe of ℂ ∖ {0}, which is path-connected because rank ℝ ℂ = 2 > 1.

theorem isPathConnected_inter_charts :
    IsPathConnected (({∞}ᶜ : Set (OnePoint ℂ)) ∩ ({((0 : ℂ) : OnePoint ℂ)}ᶜ))

simplyConnectedSpace_onePoint_of_vanKampen

OnePoint ℂ is simply connected — modulo the abstract two-open van Kampen engine. Every side-condition (path-connectivity, the two simply-connected charts, the cover equation, the path-connected overlap) is discharged above; only vanKampen itself — Seifert–van Kampen for a two-element open cover, absent from Mathlib — is taken as input.

theorem simplyConnectedSpace_onePoint_of_vanKampen (vanKampen : TwoOpenVanKampen) :
    SimplyConnectedSpace (OnePoint ℂ)

simplyConnectedSpace_sphere_of_vanKampen

The Euclidean 2-sphere S² ⊆ ℝ³ is simply connected — modulo the same engine. Transports simplyConnectedSpace_onePoint_of_vanKampen along homeoSphere : OnePoint ℂ ≃ₜ S² (simple-connectivity is a homeomorphism invariant). This is *exactly* the hypothesis that Jacobians.simplyConnectedSpace_of_homeo_sphere and genus_zero_of_nonempty_homeo_sphere consume; supplying TwoOpenVanKampen discharges #1b's backward simple-connectivity input.

theorem simplyConnectedSpace_sphere_of_vanKampen (vanKampen : TwoOpenVanKampen) :
    SimplyConnectedSpace (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1)