The Čech diagram of a family of open sets

For a family U : ι → Opens X, the Čech index category consists of the nonempty finite subsets of ι, ordered by reverse inclusion. An index s represents the intersection ⋂ i ∈ s, U i; reverse inclusion makes the evident inclusions of intersections into morphisms in Opens X.

This file constructs the resulting diagrams in open sets and topological spaces, together with the natural transformation formed by the inclusions of the finite intersections into X.

References

• R. Brown, Topology and Groupoids, Chapters 6--7.
• T. Zhu, mathlib4#41603, whose open-set and fundamental-groupoid object and map shapes guide this interface.

@[reducible, inline]

abbrev TauCeti.TopCat.CechIndex (ι : Type u) : Type u

The indices for the Čech diagram of a family of open sets: nonempty finite subsets of the indexing type, ordered by reverse inclusion.

Equations

• TauCeti.TopCat.CechIndex ι = { s : Finset ι // s.Nonempty }ᵒᵈ

def TauCeti.TopCat.CechIndex.singleton {ι : Type u} (i : ι) : CechIndex ι

The Čech index consisting of one family member.

Equations

• TauCeti.TopCat.CechIndex.singleton i = OrderDual.toDual ⟨{i}, ⋯⟩

@[simp]

theorem TauCeti.TopCat.CechIndex.coe_singleton {ι : Type u} (i : ι) : ↑(singleton i) = {i}

@[simp]

theorem TauCeti.TopCat.CechIndex.le_iff {ι : Type u} {s t : CechIndex ι} : s ≤ t ↔ ↑t ⊆ ↑s

The order on Čech indices is reverse inclusion of the underlying finite sets.

def TauCeti.TopCat.cechIntersection {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (s : CechIndex ι) : TopologicalSpace.Opens ↑X

The open set represented by a Čech index: the intersection of its family members.

Equations

• TauCeti.TopCat.cechIntersection U s = (↑s).inf U

@[simp]

theorem TauCeti.TopCat.mem_cechIntersection {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (x : ↑X) (s : CechIndex ι) : x ∈ cechIntersection U s ↔ ∀ i ∈ ↑s, x ∈ U i

@[simp]

theorem TauCeti.TopCat.cechIntersection_singleton {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (i : ι) : cechIntersection U (CechIndex.singleton i) = U i

theorem TauCeti.TopCat.cechIntersection_mono {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) {s t : CechIndex ι} (h : s ≤ t) : cechIntersection U s ≤ cechIntersection U t

Enlarging the finite set of family members shrinks its intersection.

def TauCeti.TopCat.cechOpenDiagram {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor (CechIndex ι) (TopologicalSpace.Opens ↑X)

The diagram of nonempty finite intersections of a family of open sets.

Equations

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

@[simp]

theorem TauCeti.TopCat.cechOpenDiagram_obj {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (s : CechIndex ι) : (cechOpenDiagram U).obj s = cechIntersection U s

@[simp]

theorem TauCeti.TopCat.cechOpenDiagram_map {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) {s t : CechIndex ι} (f : s ⟶ t) : (cechOpenDiagram U).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE ⋯) (CategoryTheory.eqToHom ⋯))

def TauCeti.TopCat.cechTopDiagram {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor (CechIndex ι) TopCat

The topological-space Čech diagram of a family of open sets.

Equations

• TauCeti.TopCat.cechTopDiagram U = (TauCeti.TopCat.cechOpenDiagram U).comp (TopologicalSpace.Opens.toTopCat X)

@[simp]

theorem TauCeti.TopCat.cechTopDiagram_obj {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (s : CechIndex ι) : (cechTopDiagram U).obj s = ↧↥(cechIntersection U s)

@[simp]

theorem TauCeti.TopCat.cechTopDiagram_map_apply {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) {s t : CechIndex ι} (f : s ⟶ t) (x : ↑↧↥(cechIntersection U s)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((cechTopDiagram U).map f)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x)) = ⟨↑x, ⋯⟩

def TauCeti.TopCat.cechInclusion {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (s : CechIndex ι) : (cechTopDiagram U).obj s ⟶ X

The inclusion of a finite-family intersection into the ambient space.

Equations

• TauCeti.TopCat.cechInclusion U s = (TauCeti.TopCat.cechIntersection U s).inclusion'

@[simp]

theorem TauCeti.TopCat.cechInclusion_apply {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (s : CechIndex ι) (x : ↑↧↥(cechIntersection U s)) : (CategoryTheory.ConcreteCategory.hom (cechInclusion U s)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x) = ↑x

@[simp]

theorem TauCeti.TopCat.cechTopDiagram_map_comp_inclusion {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) {s t : CechIndex ι} (f : s ⟶ t) : CategoryTheory.CategoryStruct.comp ((cechTopDiagram U).map f) (cechInclusion U t) = cechInclusion U s

theorem TauCeti.TopCat.cechTopDiagram_map_comp_inclusion_assoc {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) {s t : CechIndex ι} (f : s ⟶ t) {Z : TopCat} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((cechTopDiagram U).map f) (CategoryTheory.CategoryStruct.comp (cechInclusion U t) h) = CategoryTheory.CategoryStruct.comp (cechInclusion U s) h

def TauCeti.TopCat.cechInclusionNatTrans {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) : cechTopDiagram U ⟶ (CategoryTheory.Functor.const (CechIndex ι)).obj X

The inclusions of finite-family intersections into the ambient space form a natural transformation.

Equations

• TauCeti.TopCat.cechInclusionNatTrans U = { app := TauCeti.TopCat.cechInclusion U, naturality := ⋯ }

@[simp]

theorem TauCeti.TopCat.cechInclusionNatTrans_app {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (s : CechIndex ι) : (cechInclusionNatTrans U).app s = cechInclusion U s

theorem TauCeti.TopCat.exists_mem_cechIntersection_singleton {X : TopCat} {ι : Type u} (U : ι → TopologicalSpace.Opens ↑X) (hU : TopologicalSpace.IsOpenCover U) (x : ↑X) : ∃ (i : ι), x ∈ cechIntersection U (CechIndex.singleton i)

Every point of an open cover occurs already in a singleton object of its Čech diagram.