Uniqueness for the fundamental-groupoid Čech cocone

For an open cover, a functor out of the ambient fundamental groupoid is determined by its restrictions to the finite intersections in the Čech diagram. In fact the singleton intersections suffice: subdivision of paths shows that the cover members generate every path class. This is the uniqueness part of the colimit universal property of the Čech cocone.

The path-generation argument is the groupoid form of Brown, Topology and Groupoids, Section 6.7.

theorem TauCeti.FundamentalGroupoid.cechCocone_hom_ext_singleton {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (hU : TopologicalSpace.IsOpenCover U) {G : CategoryTheory.Grpd} {F H : (cechCocone U).pt ⟶ G} (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp ((cechCocone U).ι.app (TopCat.CechIndex.singleton i)) F = CategoryTheory.CategoryStruct.comp ((cechCocone U).ι.app (TopCat.CechIndex.singleton i)) H) : F = H

Functors out of the ambient fundamental groupoid of an open cover are determined by their composites with the singleton legs of the Čech cocone.

theorem TauCeti.FundamentalGroupoid.cechCocone_hom_ext {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (hU : TopologicalSpace.IsOpenCover U) {G : CategoryTheory.Grpd} {F H : (cechCocone U).pt ⟶ G} (h : ∀ (s : TopCat.CechIndex ι), CategoryTheory.CategoryStruct.comp ((cechCocone U).ι.app s) F = CategoryTheory.CategoryStruct.comp ((cechCocone U).ι.app s) H) : F = H

Functors out of the ambient fundamental groupoid of an open cover are determined by their composites with all the legs of the Čech cocone.