Topological Kőnig's lemma

A topological version of Kőnig's lemma is that the inverse limit of nonempty compact Hausdorff spaces is nonempty. (Note: this can be generalized further to inverse limits of nonempty compact T0 spaces, where all the maps are closed maps; see [Stone1979] --- however there is an erratum for Theorem 4 that the element in the inverse limit can have cofinally many components that are not closed points.)

We give this in a more general form, which is that cofiltered limits of nonempty compact Hausdorff spaces are nonempty (nonempty_limitCone_of_compact_t2_cofiltered_system).

This also applies to inverse limits, where {J : Type u} [Preorder J] [IsDirected J (≤)] and F : Jᵒᵖ ⥤ TopCat.

The theorem is specialized to nonempty finite types (which are compact Hausdorff with the discrete topology) in lemmas nonempty_sections_of_finite_cofiltered_system and nonempty_sections_of_finite_inverse_system in the file Mathlib.CategoryTheory.CofilteredSystem.

(See for the Set version.)

def TopCat.partialSections {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) {G : Finset J} (H : Finset (TopCat.FiniteDiagramArrow G)) : Set ((j : J) → ↑(F.toPrefunctor.obj j))

Partial sections of a cofiltered limit are sections when restricted to a finite subset of objects and morphisms of J.

Equations

• TopCat.partialSections F H = {u : (j : J) → ↑(F.toPrefunctor.obj j) | ∀ {f : TopCat.FiniteDiagramArrow G}, f ∈ H → (F.toPrefunctor.map f.snd.snd.snd.snd) (u f.fst) = u f.snd.fst}

theorem TopCat.partialSections.nonempty {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) [CategoryTheory.IsCofilteredOrEmpty J] [h : ∀ (j : J), Nonempty ↑(F.toPrefunctor.obj j)] {G : Finset J} (H : Finset (TopCat.FiniteDiagramArrow G)) : Set.Nonempty (TopCat.partialSections F H)

theorem TopCat.partialSections.directed {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) : Directed Superset fun (G : TopCat.FiniteDiagram J) => TopCat.partialSections F G.snd

theorem TopCat.partialSections.closed {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) [∀ (j : J), T2Space ↑(F.toPrefunctor.obj j)] {G : Finset J} (H : Finset (TopCat.FiniteDiagramArrow G)) : IsClosed (TopCat.partialSections F H)

theorem TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty ↑(F.toPrefunctor.obj j)] [∀ (j : J), CompactSpace ↑(F.toPrefunctor.obj j)] [∀ (j : J), T2Space ↑(F.toPrefunctor.obj j)] : Nonempty ↑(TopCat.limitCone F).pt

Cofiltered limits of nonempty compact Hausdorff spaces are nonempty topological spaces.