The groupoid van Kampen theorem

For an open cover U of a topological space X, the fundamental groupoid of X is the colimit, in the category of groupoids, of the fundamental groupoids of the nonempty finite intersections of members of U, along the inclusions of intersections. No connectedness assumption is made on the members of the cover or on their intersections.

The functor induced by a cocone is TauCeti.FundamentalGroupoid.glue, applied to the legs of the cocone at the singleton indices: these are functors out of the fundamental groupoids of the members of the cover which agree on pairwise intersections, because both factor through the leg at the corresponding two-element index. Its uniqueness is TauCeti.FundamentalGroupoid.eq_glue. With this theorem, the naturality statements of TauCeti.AlgebraicTopology.FundamentalGroupoid.Cech.Map apply to every open cover.

Main results

• TauCeti.FundamentalGroupoid.isColimitCechCocone: the Čech cocone of an open cover is a colimit cocone in the category of groupoids.

References

• R. Brown, Topology and Groupoids, 3rd ed., Section 6.7.
• T. Zhu, mathlib4#41603, whose fundamental-groupoid cosheaf interface guides the colimit formulation.

noncomputable def TauCeti.FundamentalGroupoid.isColimitCechCocone {X : TopCat} {ι : Type u} {U : ι → TopologicalSpace.Opens ↑X} (hU : TopologicalSpace.IsOpenCover U) : CategoryTheory.Limits.IsColimit (cechCocone U)

The groupoid van Kampen theorem. For an open cover of X, the fundamental groupoid of X is the colimit of the fundamental groupoids of the nonempty finite intersections of members of the cover.

Equations

• One or more equations did not get rendered due to their size.