The left piece of the matched cover is the previous punctured plane

Disproved

BraidsLinksMCG.puncturedPlane_standardGen_matched_cover_left_factor_free_v1

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

braidscoverfundamental-groupvan-kampen

The left piece of the matched cover, namely the set of points of the plane punctured at 1, ..., n+1 whose real part is below n+1, together with the open upper half-plane and the half-unit disc about n+2, has the same fundamental group as the plane punctured at 1, ..., n, and the correspondence carries the j-th standard loop of the smaller plane to the j-th standard loop of the larger one. The left piece is the smaller punctured plane together with an added collar: the upper half-plane and the disc are attached along sets that contain no puncture, so adding them does not change the fundamental group. This supplies the left algebraic input, and the hypothesis ih identifies the smaller plane's group with a free group on Fin n, that the Proved theorem b4be88b4-6dc7-4a43-80ef-4cacfa15d3de needs in order to conclude that the standard generators of the larger plane generate its fundamental group freely.

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_standardGen_matched_cover_left_factor_free_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)
    (hpcFalse : IsPathConnected (A Bool.false)) :
    ∃ fold : PuncturedPlaneGroup n ≃* FundamentalGroup (A Bool.false)
        (basept A (basePunctured (n + 1)) hx Bool.false),
      ∀ j : Fin n,
        inclHom A (basePunctured (n + 1)) hx Bool.false
            (fold (standardGen n j)) =
          standardGen (n + 1) j.castSucc := by sorry

end BraidsLinksMCG

Source

A. Hatcher, Algebraic Topology (2002), Section 1.2: adding a region to a space along a path-connected overlap that contains no puncture does not change the fundamental group, by van Kampen applied to a cover whose overlap is simply connected. Here the left piece is the punctured plane for the punctures 1, ..., n, together with the open upper half-plane and the open half-unit disc centred at n+2; the overlap of the added collar with the old plane lies in the open upper half-plane, which contains no puncture because every puncture ((j : Nat) + 1 : C) is real.

View graph