Covers generate the fundamental groupoid

Let U : ι → Set X be a family of subsets whose interiors cover X, that is, every point has some U i as a neighbourhood (for instance an open cover). This file proves the generation half of the groupoid Seifert--van Kampen theorem: every morphism of the fundamental groupoid of X is a composite of morphisms coming from the fundamental groupoids of the sets U i.

The proof subdivides a path by the Lebesgue number lemma on the unit interval so that each piece lies in a single U i (Path.exists_monotone_range_subpath_subset), and then uses Mathlib's homotopy between a path and the concatenation of its consecutive subpaths.

Main results

• TauCeti.FundamentalGroupoid.iSup_im_map_subtypeVal_eq_top: the images of the inclusion functors FundamentalGroupoid (U i) ⥤ FundamentalGroupoid X generate the whole fundamental groupoid as a subgroupoid.
• TauCeti.FundamentalGroupoid.functor_ext: two functors out of FundamentalGroupoid X which agree after precomposition with every inclusion functor are equal. This is the uniqueness part of the universal property of the fundamental groupoid as a colimit over the cover.

References

• R. Brown, Topology and Groupoids, Section 6.7.
• A. Hatcher, Algebraic Topology, Section 1.2, proof of Theorem 1.20.
• T. Zhu, mathlib4#41603, whose fundamental-groupoid cosheaf interface guides the colimit formulation.

theorem TauCeti.FundamentalGroupoid.iSup_im_map_subtypeVal_eq_top {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {U : ι → Set X} (hU : ∀ (x : X), ∃ (i : ι), U i ∈ nhds x) : ⨆ (i : ι), CategoryTheory.Subgroupoid.im (FundamentalGroupoid.map (ContinuousMap.subtypeVal (U i))) ⋯ = ⊤

Generation half of the groupoid van Kampen theorem. If every point of X has some U i as a neighbourhood, then the images of the inclusion functors FundamentalGroupoid (U i) ⥤ FundamentalGroupoid X generate the fundamental groupoid of X: every morphism is a composite of morphisms coming from the sets U i.

theorem TauCeti.FundamentalGroupoid.functor_ext {X : Type u_1} [TopologicalSpace X] {ι : Type u_2} {U : ι → Set X} (hU : ∀ (x : X), ∃ (i : ι), U i ∈ nhds x) {D : Type u_3} [CategoryTheory.Category.{u_4, u_3} D] {F G : CategoryTheory.Functor (FundamentalGroupoid X) D} (h : ∀ (i : ι), (FundamentalGroupoid.map (ContinuousMap.subtypeVal (U i))).comp F = (FundamentalGroupoid.map (ContinuousMap.subtypeVal (U i))).comp G) : F = G

Two functors out of the fundamental groupoid of X are equal as soon as they agree after precomposition with the inclusion functor of every U i, provided every point of X has some U i as a neighbourhood.