Refinements of fundamental-groupoid Čech diagrams

A chosen refinement r from a family of open sets U to a family V, with U i ⊆ V (r i), sends every finite intersection for U into the intersection for the image of its indices under r. Applying the fundamental-groupoid functor to these inclusions gives a natural transformation between the corresponding Čech diagrams.

The transformation commutes with the legs of the canonical cocones into the fundamental groupoid of the ambient space.

References

• R. Brown, Topology and Groupoids, Chapters 6--7.

noncomputable def TauCeti.FundamentalGroupoid.cechRefinementNatTrans {X : TopCat} {ι : Type u} {κ : Type v} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑X) (r : ι → κ) (hr : ∀ (i : ι), U i ≤ V (r i)) : cechDiagram U ⟶ (TopCat.CechIndex.map r).comp (cechDiagram V)

A chosen refinement induces a natural transformation between the fundamental-groupoid Čech diagrams.

Equations

• TauCeti.FundamentalGroupoid.cechRefinementNatTrans U V r hr = CategoryTheory.Functor.whiskerRight (TauCeti.TopCat.cechRefinementNatTrans U V r hr) FundamentalGroupoid.fundamentalGroupoidFunctor

@[simp]

theorem TauCeti.FundamentalGroupoid.cechRefinementNatTrans_app {X : TopCat} {ι : Type u} {κ : Type v} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑X) (r : ι → κ) (hr : ∀ (i : ι), U i ≤ V (r i)) (s : TopCat.CechIndex ι) : (cechRefinementNatTrans U V r hr).app s = FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.cechRefinement U V r hr s)

theorem TauCeti.FundamentalGroupoid.cechRefinement_comp_cocone {X : TopCat} {ι : Type u} {κ : Type v} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑X) (r : ι → κ) (hr : ∀ (i : ι), U i ≤ V (r i)) (s : TopCat.CechIndex ι) : CategoryTheory.CategoryStruct.comp ((cechRefinementNatTrans U V r hr).app s) ((cechCocone V).ι.app ((TopCat.CechIndex.map r).obj s)) = (cechCocone U).ι.app s

The natural transformation induced by a refinement commutes with the canonical cocones into the ambient fundamental groupoid.

theorem TauCeti.FundamentalGroupoid.cechRefinement_comp_cocone_assoc {X : TopCat} {ι : Type u} {κ : Type v} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑X) (r : ι → κ) (hr : ∀ (i : ι), U i ≤ V (r i)) (s : TopCat.CechIndex ι) {Z : CategoryTheory.Grpd} (h : ((CategoryTheory.Functor.const (TopCat.CechIndex κ)).obj (cechCocone V).pt).obj ((TopCat.CechIndex.map r).obj s) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cechRefinementNatTrans U V r hr).app s) (CategoryTheory.CategoryStruct.comp ((cechCocone V).ι.app ((TopCat.CechIndex.map r).obj s)) h) = CategoryTheory.CategoryStruct.comp ((cechCocone U).ι.app s) h

The natural transformation induced by a refinement commutes with the canonical cocones into the ambient fundamental groupoid.