The new standard loop generates the right half-plane factor

Proved

BraidsLinksMCG.puncturedPlane_matched_cover_right_factor_match_v1

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

algebraic-topologybraid-groupsfundamental-groupsource-faithful-childvan-kampen

For the right member of the corrected matched cover, the fundamental group at the canonical base point is pointed-equivalent to the rank-one free group, with the rank-one generator sent to the new standard loop around the last puncture. The statement records the exact generator image required by the van Kampen free-product assembly. It does not assert path-connectedness of either cover member, does not assume the Open parent, and does not use the Fadell--Neuwirth route.

Preamble

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

Formal statement

namespace BraidsLinksMCG

open Hatcher

theorem puncturedPlane_matched_cover_right_factor_match_v1 (n : ℕ)
    (A : Bool → Set (PuncturedPlane (n + 1)))
    (hx : ∀ i, basePunctured (n + 1) ∈ A i)
    (htrue :
      A Bool.true =
        {z : PuncturedPlane (n + 1) |
          ((n : ℝ) + 1) - 3 / 4 < z.1.re}) :
    ∃ (enew : FreeGroup (Fin 1) ≃*
        FundamentalGroup (A Bool.true)
          (Hatcher.basept A (basePunctured (n + 1)) hx Bool.true)),
      Hatcher.inclHom A (basePunctured (n + 1)) hx Bool.true
          (enew (FreeGroup.of (0 : Fin 1))) =
        standardGen (n + 1) (Fin.last n) := by sorry

end BraidsLinksMCG

Source

A. Hatcher, Algebraic Topology, Section 1.2, Theorem 1.20 and Example 1.21, applied to the once-punctured right half-plane in the classical inductive proof of freeness for the punctured plane.

View graph