A matched van Kampen cover for the next puncture

Proved

BraidsLinksMCG.puncturedPlane_standardGen_vankampen_cover_step_v1

by WillR · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologybraid-groupsfundamental-groupvan-kampen

For the plane with one additional puncture, construct a two-set open cover containing the canonical basepoint in both pieces. Each piece and their overlap are path-connected, and every fundamental-group class coming from either piece is a word in the named standard loops. The old-puncture piece can be formed from a left half-plane with a narrow corridor to the canonical basepoint; the new-puncture piece lies to the right. The puncture-free overlap permits van Kampen's surjectivity theorem to turn these local generation facts into generation of the whole punctured plane. The induction hypothesis identifies the old standard loops as a free basis; this statement does not assert a new free-basis relation.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_BraidsLinksMCG_StandardLoops
import Definitions.Def_Hatcher_VanKampen

Formal statement

namespace BraidsLinksMCG

theorem puncturedPlane_standardGen_vankampen_cover_step_v1 (n : ℕ)
    (ih : ∃ e : PuncturedPlaneGroup n ≃* FreeGroup (Fin n),
      ∀ j : Fin n, e (standardGen n j) = FreeGroup.of j) :
    ∃ (A : Bool → Set (PuncturedPlane (n + 1)))
      (hx : ∀ i, basePunctured (n + 1) ∈ A i),
      (∀ i, IsOpen (A i)) ∧
      (∀ i, IsPathConnected (A i)) ∧
      (⋃ i, A i) = Set.univ ∧
      (∀ i j, IsPathConnected (A i ∩ A j)) ∧
      (∀ i, (Hatcher.inclHom A (basePunctured (n + 1)) hx i).range ≤
        (FreeGroup.lift (standardGen (n + 1))).range) := by sorry

end BraidsLinksMCG

Source

A. Hatcher, Algebraic Topology (2002), Section 1.2, Theorem 1.20 and Example 1.21, pp. 43-46; explicit two-region cover and named-loop matching for the punctured plane.

View graph