Maps of topological Čech diagrams

A continuous map between spaces, together with a map of cover indices that carries each source open into the corresponding target open, induces a natural transformation between their Čech diagrams. The transformation commutes with the canonical inclusions of the intersections into the ambient spaces.

These maps provide the topological input for naturality of constructions obtained by applying a functor to a Čech diagram, in particular the fundamental-groupoid van Kampen cocone.

References

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

theorem TauCeti.TopCat.mapsTo_cechIntersection {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 : CechIndex ι) : Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) ↑(cechIntersection U s) ↑(cechIntersection V ((CechIndex.map r).obj s))

A map of covered spaces carries an intersection in the source Čech diagram into the intersection indexed by the corresponding image in the target diagram.

def TauCeti.TopCat.cechMap {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 : CechIndex ι) : (cechTopDiagram U).obj s ⟶ (cechTopDiagram V).obj ((CechIndex.map r).obj s)

The map between two Čech intersections induced by a map of covered spaces.

Equations

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

theorem TauCeti.TopCat.cechMap_comp_inclusion {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 : CechIndex ι) : CategoryTheory.CategoryStruct.comp (cechMap U V f r hf s) (cechInclusion V ((CechIndex.map r).obj s)) = CategoryTheory.CategoryStruct.comp (cechInclusion U s) f

Maps between Cech intersections commute with their inclusions into the ambient spaces.

theorem TauCeti.TopCat.cechMap_comp_inclusion_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 : CechIndex ι) {Z : TopCat} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (cechMap U V f r hf s) (CategoryTheory.CategoryStruct.comp (cechInclusion V ((CechIndex.map r).obj s)) h) = CategoryTheory.CategoryStruct.comp (cechInclusion U s) (CategoryTheory.CategoryStruct.comp f h)

Maps between Cech intersections commute with their inclusions into the ambient spaces.

@[simp]

theorem TauCeti.TopCat.cechMap_apply {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 : CechIndex ι) (x : ↑↧↥(cechIntersection U s)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom (cechMap U V f r hf s)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x)) = ⟨(CategoryTheory.ConcreteCategory.hom f) ↑x, ⋯⟩

def TauCeti.TopCat.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))) : cechTopDiagram U ⟶ (CechIndex.map r).comp (cechTopDiagram V)

The intersection maps associated to a map of covered spaces form a natural transformation between the two Čech diagrams.

Equations

• TauCeti.TopCat.cechMapNatTrans U V f r hf = { app := TauCeti.TopCat.cechMap U V f r hf, naturality := ⋯ }

@[simp]

theorem TauCeti.TopCat.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 : CechIndex ι) : (cechMapNatTrans U V f r hf).app s = cechMap U V f r hf s