13.7. SphereTopology.VanKampen🔗

Jacobians.SphereTopology.VanKampen — source

telescope

Telescoping. Given junctions q, spokes c k : ⟦o ⤳ q k⟧, arcs F, and the hypothesis that each conjugated loop c kᵢ · F k · c kᵢ₊₁⁻¹ is the identity at o, the concatenation of the arcs, conjugated by the two end spokes, is the identity at o. Proved by induction on the number of arcs, cancelling the inner c⁻¹ · c pairs.

theorem telescope {o : Z} :
    ∀ {n : ℕ} (q : Fin (n + 1) → Z) (c : (k : Fin (n + 1)) → Q o (q k))
      (F : (k : Fin n) → Path (q k.castSucc) (q k.succ)),
      (∀ k : Fin n,
        trans (c k.castSucc) (trans (mk (F k)) (symm (c k.succ)))
          = Path.Homotopic.Quotient.refl o) →
      trans (c 0) (trans (mk (Path.concat q F)) (symm (c (last n))))
        = Path.Homotopic.Quotient.refl o

cancel_conj

Groupoid cancellation: from a · (x · b⁻¹) = id conclude x = a⁻¹ · b. (Conjugation by the end spokes is undone.)

theorem cancel_conj {o p r : Z} (a : Q o p) (x : Q p r) (b : Q o r)
    (h : trans a (trans x (symm b)) = Path.Homotopic.Quotient.refl o) :
    x = trans (symm a) b

concat_nullhomotopic

Loop-chain nullhomotopy (Path level). A loop presented as the concatenation of arcs F with junctions q (both ends at o, via h0, hl), equipped with spokes spoke j : o ⤳ q j whose two ends are the constant path (retyped) and for which every conjugated loop spoke kᵢ · F k · spoke kᵢ₊₁⁻¹ is nullhomotopic, is itself nullhomotopic. This re-expresses telescope via mk, isolating the homotopy-theory input (hloop) from the groupoid algebra.

theorem concat_nullhomotopic {o : Z} {n : ℕ} (q : Fin (n + 1) → Z)
    (F : (k : Fin n) → Path (q k.castSucc) (q k.succ)) (h0 : q 0 = o) (hl : q (last n) = o)
    (spoke : (j : Fin (n + 1)) → Path o (q j))
    (hs0 : spoke 0 = (Path.refl o).cast rfl h0)
    (hsl : spoke (last n) = (Path.refl o).cast rfl hl)
    (hloop : ∀ k : Fin n,
      Path.Homotopic ((spoke k.castSucc).trans ((F k).trans (spoke k.succ).symm))
        (Path.refl o)) :
    Path.Homotopic (Path.concat q F) ((Path.refl o).cast h0 hl)

nullhomotopic_of_mem_isSimplyConnected

A loop lying entirely in a simply-connected set W is nullhomotopic in the ambient space.

theorem nullhomotopic_of_mem_isSimplyConnected {W : Set Z} (hW : IsSimplyConnected W) {o : Z}
    (L : Path o o) (hL : ∀ t, L t ∈ W) : Path.Homotopic L (Path.refl o)

exists_lebesgue_subdivision

Lebesgue subdivision of a loop. For a continuous γ : I → Z and an open cover {U, V} of Z, there is a uniform subdivision t k = k/(n+1) of [0,1] (so t 0 = 0, t (last n) = 1) such that each closed piece γ '' [t kᵢ, t kᵢ₊₁] lies entirely in U or in V.

theorem exists_lebesgue_subdivision {γ : I → Z} (hγ : Continuous γ) {U V : Set Z}
    (hU : IsOpen U) (hV : IsOpen V) (hcov : U ∪ V = Set.univ) :
    ∃ (n : ℕ) (t : Fin (n + 1) → I), t 0 = 0 ∧ t (last n) = 1 ∧
      ∀ k : Fin n, (γ '' (Set.uIcc (t k.castSucc) (t k.succ)) ⊆ U) ∨
        (γ '' (Set.uIcc (t k.castSucc) (t k.succ)) ⊆ V)

loop_at_overlap_nullhomotopic

Loops at a basepoint in the overlap are nullhomotopic. If Z is covered by two open simply-connected sets U, V with path-connected intersection U ∩ V, then every loop based at a point o ∈ U ∩ V is nullhomotopic. This is the analytic heart: Lebesgue-subdivide the loop into arcs each inside one chart, connect the junctions to o through the appropriate chart (the *spokes*), nullhomotope each conjugated arc inside its chart, and telescope.

theorem loop_at_overlap_nullhomotopic {U V : Set Z} (hU : IsOpen U) (hV : IsOpen V)
    (hcov : U ∪ V = Set.univ) (hUsc : IsSimplyConnected U) (hVsc : IsSimplyConnected V)
    (hUV : IsPathConnected (U ∩ V)) {o : Z} (hoUV : o ∈ U ∩ V) (γ : Path o o) :
    Path.Homotopic γ (Path.refl o)

twoOpenVanKampen_holds

Two-open van Kampen. A path-connected space that is the union of two open simply-connected sets with path-connected intersection is simply connected. (This is exactly the abstract engine Jacobians.RiemannSphere.TwoOpenVanKampen.)

theorem twoOpenVanKampen_holds : Jacobians.RiemannSphere.TwoOpenVanKampen