Maps of fundamental-groupoid Čech diagrams

A map of covered spaces induces a natural transformation between the corresponding fundamental-groupoid Čech diagrams. Its components commute with the canonical cocones into the ambient fundamental groupoids. Thus a natural map on the eventual Čech colimits is forced to be the usual map on fundamental groupoids.

References

• R. Brown, Topology and Groupoids, Chapters 6--7.
• T. Zhu, mathlib4#41603, whose fundamental-groupoid cosheaf interface guides the colimit formulation.

noncomputable def TauCeti.FundamentalGroupoid.cechMapNatTrans {X Y : TopCat} {ι : Type u} {κ : Type z} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) ↑(U i) ↑(V (r i))) : cechDiagram U ⟶ (TopCat.CechIndex.map r).comp (cechDiagram V)

A map of covered spaces induces a natural transformation between the corresponding fundamental-groupoid Čech diagrams.

Equations

• TauCeti.FundamentalGroupoid.cechMapNatTrans U V f r hf = CategoryTheory.Functor.whiskerRight (TauCeti.TopCat.cechMapNatTrans U V f r hf) FundamentalGroupoid.fundamentalGroupoidFunctor

@[simp]

theorem TauCeti.FundamentalGroupoid.cechMapNatTrans_app {X Y : TopCat} {ι : Type u} {κ : Type z} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) ↑(U i) ↑(V (r i))) (s : TopCat.CechIndex ι) : (cechMapNatTrans U V f r hf).app s = FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.cechMap U V f r hf s)

theorem TauCeti.FundamentalGroupoid.cechMap_comp_cocone {X Y : TopCat} {ι : Type u} {κ : Type z} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) ↑(U i) ↑(V (r i))) (s : TopCat.CechIndex ι) : CategoryTheory.CategoryStruct.comp ((cechMapNatTrans U V f r hf).app s) ((cechCocone V).ι.app ((TopCat.CechIndex.map r).obj s)) = CategoryTheory.CategoryStruct.comp ((cechCocone U).ι.app s) (FundamentalGroupoid.fundamentalGroupoidFunctor.map f)

The natural transformation induced by a map of covered spaces commutes with the canonical cocones into the ambient fundamental groupoids.

theorem TauCeti.FundamentalGroupoid.cechMap_comp_cocone_assoc {X Y : TopCat} {ι : Type u} {κ : Type z} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) ↑(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 ((cechMapNatTrans U V f r hf).app s) (CategoryTheory.CategoryStruct.comp ((cechCocone V).ι.app ((TopCat.CechIndex.map r).obj s)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((cechCocone U).ι.app s) (FundamentalGroupoid.fundamentalGroupoidFunctor.map f)) h

The natural transformation induced by a map of covered spaces commutes with the canonical cocones into the ambient fundamental groupoids.

noncomputable def TauCeti.FundamentalGroupoid.cechMapCocone {X Y : TopCat} {ι : Type u} {κ : Type z} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) ↑(U i) ↑(V (r i))) : CategoryTheory.Limits.Cocone (cechDiagram U)

The target Čech cocone, restricted along a map of covered spaces, as a cocone on the source Čech diagram.

Equations

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

@[simp]

theorem TauCeti.FundamentalGroupoid.cechMapCocone_pt {X Y : TopCat} {ι : Type u} {κ : Type z} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) ↑(U i) ↑(V (r i))) : (cechMapCocone U V f r hf).pt = (cechCocone V).pt

@[simp]

theorem TauCeti.FundamentalGroupoid.cechMapCocone_ι_app {X Y : TopCat} {ι : Type u} {κ : Type z} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) ↑(U i) ↑(V (r i))) (s : TopCat.CechIndex ι) : (cechMapCocone U V f r hf).ι.app s = CategoryTheory.CategoryStruct.comp ((cechMapNatTrans U V f r hf).app s) ((cechCocone V).ι.app ((TopCat.CechIndex.map r).obj s))

theorem TauCeti.FundamentalGroupoid.isColimit_desc_cechMapCocone {X Y : TopCat} {ι : Type u} {κ : Type z} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑Y) (f : X ⟶ Y) (r : ι → κ) (hf : ∀ (i : ι), Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) ↑(U i) ↑(V (r i))) (hU : CategoryTheory.Limits.IsColimit (cechCocone U)) : hU.desc (cechMapCocone U V f r hf) = FundamentalGroupoid.fundamentalGroupoidFunctor.map f

If the source canonical cocone is colimiting, then its induced map to the target canonical cocone is the usual map on fundamental groupoids. This is the map-level naturality statement needed by the Čech colimit form of van Kampen.