# mathlibdocumentation

topology.category.Top.limits

# The category of topological spaces has all limits and colimits #

Further, these limits and colimits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.

def Top.limit_cone {J : Type u} (F : J Top) :

A choice of limit cone for a functor F : J ⥤ Top. Generally you should just use limit.cone F, unless you need the actual definition (which is in terms of types.limit_cone).

Equations
def Top.limit_cone_infi {J : Type u} (F : J Top) :

A choice of limit cone for a functor F : J ⥤ Top whose topology is defined as an infimum of topologies infimum. Generally you should just use limit.cone F, unless you need the actual definition (which is in terms of types.limit_cone).

Equations
def Top.limit_cone_is_limit {J : Type u} (F : J Top) :

The chosen cone Top.limit_cone F for a functor F : J ⥤ Top is a limit cone. Generally you should just use limit.is_limit F, unless you need the actual definition (which is in terms of types.limit_cone_is_limit).

Equations
def Top.limit_cone_infi_is_limit {J : Type u} (F : J Top) :

The chosen cone Top.limit_cone_infi F for a functor F : J ⥤ Top is a limit cone. Generally you should just use limit.is_limit F, unless you need the actual definition (which is in terms of types.limit_cone_is_limit).

Equations
@[instance]
@[instance]
Equations
def Top.colimit_cocone {J : Type u} (F : J Top) :

A choice of colimit cocone for a functor F : J ⥤ Top. Generally you should just use colimit.coone F, unless you need the actual definition (which is in terms of types.colimit_cocone).

Equations
def Top.colimit_cocone_is_colimit {J : Type u} (F : J Top) :

The chosen cocone Top.colimit_cocone F for a functor F : J ⥤ Top is a colimit cocone. Generally you should just use colimit.is_colimit F, unless you need the actual definition (which is in terms of types.colimit_cocone_is_colimit).

Equations
@[instance]
@[instance]
Equations
theorem Top.is_topological_basis_cofiltered_limit {J : Type u} (F : J Top) (T : Π (j : J), set (set (F.obj j))) (hT : ∀ (j : J), ) (univ : ∀ (i : J), set.univ T i) (inter : ∀ (i : J) (U1 U2 : set (F.obj i)), U1 T iU2 T iU1 U2 T i) (compat : ∀ (i j : J) (f : i j) (V : set (F.obj j)), V T j(F.map f) ⁻¹' V T i) :
topological_space.is_topological_basis {U : set (C.X) | ∃ (j : J) (V : set (F.obj j)), V T j U = (C.π.app j) ⁻¹' V}

Given a compatible collection of topological bases for the factors in a cofiltered limit which contain set.univ and are closed under intersections, the induced naive collection of sets in the limit is, in fact, a topological basis.

## 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_limit_cone_of_compact_t2_cofiltered_system).

This also applies to inverse limits, where {J : Type u} [directed_order J] and F : Jᵒᵖ ⥤ Top.

The theorem is specialized to nonempty finite types (which are compact Hausdorff with the discrete topology) in nonempty_sections_of_fintype_cofiltered_system and nonempty_sections_of_fintype_inverse_system.

(See https://stacks.math.columbia.edu/tag/086J for the Set version.)

def Top.partial_sections {J : Type u} (F : J Top) {G : finset J} (H : finset (finite_diagram_arrow G)) :
set (Π (j : J), (F.obj j))

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

Equations
theorem Top.partial_sections.nonempty {J : Type u} (F : J Top) [h : ∀ (j : J), nonempty (F.obj j)] {G : finset J} (H : finset (finite_diagram_arrow G)) :
theorem Top.partial_sections.directed {J : Type u} (F : J Top) :
(λ (G : finite_diagram J),
theorem Top.partial_sections.closed {J : Type u} (F : J Top) [∀ (j : J), t2_space (F.obj j)] {G : finset J} (H : finset (finite_diagram_arrow G)) :
theorem Top.nonempty_limit_cone_of_compact_t2_cofiltered_system {J : Type u} (F : J Top) [∀ (j : J), nonempty (F.obj j)] [∀ (j : J), compact_space (F.obj j)] [∀ (j : J), t2_space (F.obj j)] :

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

theorem nonempty_sections_of_fintype_cofiltered_system.init {J : Type u} (F : J Type u) [hf : Π (j : J), fintype (F.obj j)] [hne : ∀ (j : J), nonempty (F.obj j)] :

This bootstraps nonempty_sections_of_fintype_inverse_system. In this version, the F functor is between categories of the same universe, and it is an easy corollary to Top.nonempty_limit_cone_of_compact_t2_inverse_system.

theorem nonempty_sections_of_fintype_cofiltered_system {J : Type u} (F : J Type v) [Π (j : J), fintype (F.obj j)] [∀ (j : J), nonempty (F.obj j)] :

The cofiltered limit of nonempty finite types is nonempty.

See nonempty_sections_of_fintype_inverse_system for a specialization to inverse limits.

theorem nonempty_sections_of_fintype_inverse_system {J : Type u} (F : Jᵒᵖ Type v) [Π (j : Jᵒᵖ), fintype (F.obj j)] [∀ (j : Jᵒᵖ), nonempty (F.obj j)] :

The inverse limit of nonempty finite types is nonempty.

See nonempty_sections_of_fintype_cofiltered_system for a generalization to cofiltered limits. That version applies in almost all cases, and the only difference is that this version allows J to be empty.

This may be regarded as a generalization of Kőnig's lemma. To specialize: given a locally finite connected graph, take Jᵒᵖ to be ℕ and F j to be length-j paths that start from an arbitrary fixed vertex. Elements of F.sections can be read off as infinite rays in the graph.