Based van Kampen for neighborhood covers

Homomorphisms out of the fundamental groups of a family whose interiors cover the space glue uniquely when they agree on each pairwise intersection, provided the triple intersections are path connected and every member contains the basepoint. Repeated triple indices imply path connectedness of the double intersections and individual members. The overlaps may differ from pair to pair. This gives the universal property needed to compute a fundamental group by successively adjoining cover members, without requiring a single common overlap. Finiteness of the family is unnecessary.

Pairwise compatibility defines transitions between local functors, and paths in triple intersections establish their cocycle law. Choosing a cover member at each point makes these functors agree on overlaps, so the fundamental-groupoid gluing theorem applies. No cover member is required to be open.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Theorem 1.20.
• R. Brown, Topology and Groupoids, 3rd ed., Section 6.7.

theorem TauCeti.existsUnique_vanKampenDesc {K : Type w} [Monoid K] {X : Type v} [TopologicalSpace X] {ι : Type u} (U : ι → Set X) (x : X) (hCover : ∀ (y : X), ∃ (i : ι), U i ∈ nhds y) (hx : ∀ (i : ι), x ∈ U i) (hTriple : ∀ (i j k : ι), IsPathConnected (U i ∩ U j ∩ U k)) (f : (i : ι) → FundamentalGroup ↑(U i) ⟨x, ⋯⟩ →* K) (hcompat : ∀ (i j : ι), (f i).comp (FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩) = (f j).comp (FundamentalGroup.map (ContinuousMap.inclusion ⋯) ⟨x, ⋯⟩)) : ∃! d : FundamentalGroup X x →* K, ∀ (i : ι), d.comp (FundamentalGroup.map (ContinuousMap.subtypeVal (U i)) ⟨x, ⋯⟩) = f i

The based van Kampen theorem for a neighborhood cover, in universal-property form. Pairwise compatible homomorphisms out of the fundamental groups of the cover members extend uniquely to the ambient fundamental group. Repeated indices in the triple-intersection hypothesis imply path connectedness of the double intersections and individual members. No common pairwise intersection is required, and the target can be any monoid.