Refinements of topological Čech diagrams

A map of indexing types r : ι → κ induces a functor between Čech index categories, sending a nonempty finite set to its image. If U i ⊆ V (r i) for all i, the inclusions of each finite intersection for U into the intersection for the image of its indices form a natural transformation between the topological Čech diagrams, compatible with the inclusions into the ambient space.

References

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

noncomputable def TauCeti.TopCat.CechIndex.map {ι : Type u} {κ : Type w} (r : ι → κ) : CategoryTheory.Functor (CechIndex ι) (CechIndex κ)

The functor on Čech index categories induced by a map of indexing types. It sends a nonempty finite set to its image.

Equations

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

@[simp]

theorem TauCeti.TopCat.CechIndex.mem_map_obj_iff {ι : Type u} {κ : Type w} (r : ι → κ) (s : CechIndex ι) (j : κ) : j ∈ ↑((map r).obj s) ↔ ∃ i ∈ ↑s, r i = j

@[simp]

theorem TauCeti.TopCat.CechIndex.map_obj_singleton {ι : Type u} {κ : Type w} (r : ι → κ) (i : ι) : (map r).obj (singleton i) = singleton (r i)

theorem TauCeti.TopCat.cechIntersection_le_refinement {X : TopCat} {ι : Type u} {κ : Type w} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑X) (r : ι → κ) (hr : ∀ (i : ι), U i ≤ V (r i)) (s : CechIndex ι) : cechIntersection U s ≤ cechIntersection V ((CechIndex.map r).obj s)

The intersection indexed by s in a finer family is contained in the intersection indexed by the image of s in a coarser family.

noncomputable def TauCeti.TopCat.cechRefinement {X : TopCat} {ι : Type u} {κ : Type w} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑X) (r : ι → κ) (hr : ∀ (i : ι), U i ≤ V (r i)) (s : CechIndex ι) : (cechTopDiagram U).obj s ⟶ (cechTopDiagram V).obj ((CechIndex.map r).obj s)

The inclusion from an intersection in a finer family to the corresponding intersection in a coarser family.

Equations

• TauCeti.TopCat.cechRefinement U V r hr s = (TopologicalSpace.Opens.toTopCat X).map (CategoryTheory.homOfLE ⋯)

theorem TauCeti.TopCat.cechRefinement_comp_inclusion {X : TopCat} {ι : Type u} {κ : Type w} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑X) (r : ι → κ) (hr : ∀ (i : ι), U i ≤ V (r i)) (s : CechIndex ι) : CategoryTheory.CategoryStruct.comp (cechRefinement U V r hr s) (cechInclusion V ((CechIndex.map r).obj s)) = cechInclusion U s

Refinement inclusions commute with the canonical inclusions of Čech intersections into the ambient space.

theorem TauCeti.TopCat.cechRefinement_comp_inclusion_assoc {X : TopCat} {ι : Type u} {κ : Type w} (U : ι → TopologicalSpace.Opens ↑X) (V : κ → TopologicalSpace.Opens ↑X) (r : ι → κ) (hr : ∀ (i : ι), U i ≤ V (r i)) (s : CechIndex ι) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (cechRefinement U V r hr s) (CategoryTheory.CategoryStruct.comp (cechInclusion V ((CechIndex.map r).obj s)) h) = CategoryTheory.CategoryStruct.comp (cechInclusion U s) h

Refinement inclusions commute with the canonical inclusions of Čech intersections into the ambient space.

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

The inclusions associated to a chosen refinement form a natural transformation between the two topological Čech diagrams.

Equations

• TauCeti.TopCat.cechRefinementNatTrans U V r hr = { app := TauCeti.TopCat.cechRefinement U V r hr, naturality := ⋯ }

@[simp]

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