The fundamental-groupoid Čech diagram of a family of open sets

For a family U : ι → Opens X, this file maps its topological Čech diagram through the fundamental-groupoid functor and constructs the canonical cocone to the fundamental groupoid of X. The cocone is the input for the groupoid van Kampen colimit theorem.

References

• R. Brown, Topology and Groupoids, Chapters 6--7.
• T. Zhu, mathlib4#41603, whose open-set and fundamental-groupoid object and map shapes guide this interface.

noncomputable def TauCeti.FundamentalGroupoid.cechDiagram {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor (TopCat.CechIndex ι) CategoryTheory.Grpd

The fundamental-groupoid Čech diagram of a family of open sets.

Equations

• TauCeti.FundamentalGroupoid.cechDiagram U = (TauCeti.TopCat.cechTopDiagram U).comp FundamentalGroupoid.fundamentalGroupoidFunctor

@[simp]

theorem TauCeti.FundamentalGroupoid.cechDiagram_obj {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (s : TopCat.CechIndex ι) : (cechDiagram U).obj s = FundamentalGroupoid.fundamentalGroupoidFunctor.obj ↧↥(TopCat.cechIntersection U s)

@[simp]

theorem TauCeti.FundamentalGroupoid.cechDiagram_map {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) {s t : TopCat.CechIndex ι} (f : s ⟶ t) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((cechDiagram U).map f) (CategoryTheory.eqToHom ⋯)) = FundamentalGroupoid.fundamentalGroupoidFunctor.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((TopCat.cechTopDiagram U).map f) (CategoryTheory.eqToHom ⋯)))

noncomputable def TauCeti.FundamentalGroupoid.cechCocone {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.Cocone (cechDiagram U)

The canonical cocone from the Čech diagram to the fundamental groupoid of the ambient space.

Equations

• TauCeti.FundamentalGroupoid.cechCocone U = FundamentalGroupoid.fundamentalGroupoidFunctor.mapCocone { pt := X, ι := TauCeti.TopCat.cechInclusionNatTrans U }

@[simp]

theorem TauCeti.FundamentalGroupoid.cechCocone_pt {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) : (cechCocone U).pt = FundamentalGroupoid.fundamentalGroupoidFunctor.obj X

@[simp]

theorem TauCeti.FundamentalGroupoid.cechCocone_ι_app {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (s : TopCat.CechIndex ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((cechCocone U).ι.app s) (CategoryTheory.eqToHom ⋯)) = FundamentalGroupoid.fundamentalGroupoidFunctor.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (TopCat.cechInclusion U s))