Documentation

Mathlib.Topology.Category.TopCat.Limits.Konig

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 [Sto79] --- 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 https://stacks.math.columbia.edu/tag/086J for the Set version.)

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

Equations
Instances For
    theorem TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty (F.obj j)] [∀ (j : J), CompactSpace (F.obj j)] [∀ (j : J), T2Space (F.obj j)] :

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