mathlib documentation

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.

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

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

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

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

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

def Top.partial_sections {J : Type u} [directed_order J] (F : Jᵒᵖ Top) (j : Jᵒᵖ) :
set (Π (j : Jᵒᵖ), (F.obj j))

The partial sections of an inverse system of topological spaces from an index j are sections when restricted to all objects less than or equal to j.

Equations
theorem Top.partial_sections.nonempty {J : Type u} [directed_order J] (F : Jᵒᵖ Top) [∀ (j : Jᵒᵖ), nonempty (F.obj j)] (j : Jᵒᵖ) :
theorem Top.partial_sections.closed {J : Type u} [directed_order J] (F : Jᵒᵖ Top) [∀ (j : Jᵒᵖ), t2_space (F.obj j)] (j : Jᵒᵖ) :
theorem Top.nonempty_limit_cone_of_compact_t2_inverse_system {J : Type u} [directed_order J] (F : Jᵒᵖ Top) [∀ (j : Jᵒᵖ), nonempty (F.obj j)] [∀ (j : Jᵒᵖ), compact_space (F.obj j)] [∀ (j : Jᵒᵖ), t2_space (F.obj j)] :