Covers by path-connected sets generate the fundamental group

Let U : ι → Set X be a family of subsets whose interiors cover X, all containing the basepoint x, such that every pairwise intersection U i ∩ U j (in particular every U i) is path connected. Then π₁(X, x) is generated by the images of the groups π₁(U i, x) under the inclusions. This is the surjectivity half of the Seifert--van Kampen theorem: the canonical map from the free product of the π₁(U i, x) to π₁(X, x) is surjective.

The result applies when a cover has path-connected pairwise intersections, allowing loops in X to be expressed using loops in the covering sets. It follows from the groupoid generation theorem TauCeti.FundamentalGroupoid.iSup_im_map_subtypeVal_eq_top.

Path-connectedness of the pairwise intersections cannot be dropped: the circle is the union of two open arcs, each simply connected, whose intersection has two components.

Main results

• TauCeti.FundamentalGroup.iSup_range_map_subtypeVal_eq_top: the images of the fundamental groups of the members of the cover generate π₁(X, x).
• TauCeti.FundamentalGroup.range_map_subtypeVal_sup_eq_top: the same statement for a cover by two sets A, B with A, B and A ∩ B path connected.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Theorem 1.20, the proof that the map Φ is surjective.
• R. Brown, Topology and Groupoids, Section 6.7.

@[simp]

theorem TauCeti.FundamentalGroup.iSup_range_map_subtypeVal_eq_top {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {U : ι → Set X} {x : X} (hU : ∀ (y : X), ∃ (i : ι), U i ∈ nhds y) (hx : ∀ (i : ι), x ∈ U i) (hpc : ∀ (i j : ι), IsPathConnected (U i ∩ U j)) : ⨆ (i : ι), (FundamentalGroup.map (ContinuousMap.subtypeVal (U i)) ⟨x, ⋯⟩).range = ⊤

Generation half of the Seifert--van Kampen theorem. Let the interiors of the sets U i cover X, let every U i contain x, and let every intersection U i ∩ U j be path connected. Then π₁(X, x) is generated by the images of the fundamental groups π₁(U i, x) under the inclusions.

@[simp]

theorem TauCeti.FundamentalGroup.range_map_subtypeVal_sup_eq_top {X : Type u_1} [TopologicalSpace X] {x : X} {A B : Set X} (hAB : interior A ∪ interior B = Set.univ) (hA : IsPathConnected A) (hB : IsPathConnected B) (hAB' : IsPathConnected (A ∩ B)) (hxA : x ∈ A) (hxB : x ∈ B) : (FundamentalGroup.map (ContinuousMap.subtypeVal A) ⟨x, hxA⟩).range ⊔ (FundamentalGroup.map (ContinuousMap.subtypeVal B) ⟨x, hxB⟩).range = ⊤

Generation half of the Seifert--van Kampen theorem, for two sets. If the interiors of A and B cover X, and A, B and A ∩ B are path connected and contain x, then π₁(X, x) is generated by the images of π₁(A, x) and π₁(B, x) under the inclusions.