# 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 v} (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 v} (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 v} (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 v} (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
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
def Top.colimit_cocone {J : Type v} (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 v} (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
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[reducible]
def Top.pi_π {ι : Type v} (α : ι Top) (i : ι) :
Top.of (Π (i : ι), (α i)) α i

The projection from the product as a bundled continous map.

@[simp]
theorem Top.pi_fan_X {ι : Type v} (α : ι Top) :
(Top.pi_fan α).X = Top.of (Π (i : ι), (α i))
def Top.pi_fan {ι : Type v} (α : ι Top) :

The explicit fan of a family of topological spaces given by the pi type.

Equations
@[simp]
theorem Top.pi_fan_π_app {ι : Type v} (α : ι Top) (X : category_theory.discrete ι) :
(Top.pi_fan α).π.app X = X.as
def Top.pi_fan_is_limit {ι : Type v} (α : ι Top) :

The constructed fan is indeed a limit

Equations
noncomputable def Top.pi_iso_pi {ι : Type v} (α : ι Top) :
α Top.of (Π (i : ι), (α i))

The product is homeomorphic to the product of the underlying spaces, equipped with the product topology.

Equations
@[simp]
theorem Top.pi_iso_pi_inv_π_assoc {ι : Type v} (α : ι Top) (i : ι) {X' : Top} (f' : α i X') :
.inv = i f'
@[simp]
theorem Top.pi_iso_pi_inv_π {ι : Type v} (α : ι Top) (i : ι) :
= i
@[simp]
theorem Top.pi_iso_pi_inv_π_apply {ι : Type v} (α : ι Top) (i : ι) (x : Π (i : ι), (α i)) :
(((Top.pi_iso_pi α).inv) x) = x i
@[simp]
theorem Top.pi_iso_pi_hom_apply {ι : Type v} (α : ι Top) (i : ι) (x : α) :
((Top.pi_iso_pi α).hom) x i = x
@[reducible]
def Top.sigma_ι {ι : Type v} (α : ι Top) (i : ι) :
α i Top.of (Σ (i : ι), (α i))

The inclusion to the coproduct as a bundled continous map.

def Top.sigma_cofan {ι : Type v} (α : ι Top) :

The explicit cofan of a family of topological spaces given by the sigma type.

Equations
@[simp]
theorem Top.sigma_cofan_X {ι : Type v} (α : ι Top) :
.X = Top.of (Σ (i : ι), (α i))
@[simp]
theorem Top.sigma_cofan_ι_app {ι : Type v} (α : ι Top) (X : category_theory.discrete ι) :
.ι.app X = X.as
def Top.sigma_cofan_is_colimit {ι : Type v} (α : ι Top) :

The constructed cofan is indeed a colimit

Equations
noncomputable def Top.sigma_iso_sigma {ι : Type v} (α : ι Top) :
α Top.of (Σ (i : ι), (α i))

The coproduct is homeomorphic to the disjoint union of the topological spaces.

Equations
@[simp]
theorem Top.sigma_iso_sigma_hom_ι {ι : Type v} (α : ι Top) (i : ι) :
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_assoc {ι : Type v} (α : ι Top) (i : ι) {X' : Top} (f' : Top.of (Σ (i : ι), (α i)) X') :
= i f'
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_apply {ι : Type v} (α : ι Top) (i : ι) (x : (α i)) :
.hom) x) = i, x⟩
@[simp]
theorem Top.sigma_iso_sigma_inv_apply {ι : Type v} (α : ι Top) (i : ι) (x : (α i)) :
.inv) i, x⟩ =
theorem Top.induced_of_is_limit {J : Type v} {F : J Top}  :
theorem Top.limit_topology {J : Type v} (F : J Top) :
@[reducible]
def Top.prod_fst {X Y : Top} :

The first projection from the product.

@[reducible]
def Top.prod_snd {X Y : Top} :

The second projection from the product.

def Top.prod_binary_fan (X Y : Top) :

The explicit binary cofan of X, Y given by X × Y.

Equations

The constructed binary fan is indeed a limit

Equations
noncomputable def Top.prod_iso_prod (X Y : Top) :

The homeomorphism between X ⨯ Y and the set-theoretic product of X and Y, equipped with the product topology.

Equations
@[simp]
theorem Top.prod_iso_prod_hom_fst (X Y : Top) :
@[simp]
theorem Top.prod_iso_prod_hom_fst_assoc (X Y : Top) {X' : Top} (f' : X X') :
@[simp]
theorem Top.prod_iso_prod_hom_snd (X Y : Top) :
@[simp]
theorem Top.prod_iso_prod_hom_snd_assoc (X Y : Top) {X' : Top} (f' : Y X') :
@[simp]
theorem Top.prod_iso_prod_hom_apply {X Y : Top} (x : (X Y)) :
@[simp]
theorem Top.prod_iso_prod_inv_fst_assoc (X Y : Top) {X' : Top} (f' : X X') :
=
@[simp]
theorem Top.prod_iso_prod_inv_fst (X Y : Top) :
@[simp]
theorem Top.prod_iso_prod_inv_snd (X Y : Top) :
@[simp]
theorem Top.prod_iso_prod_inv_snd_assoc (X Y : Top) {X' : Top} (f' : Y X') :
=
theorem Top.range_prod_map {W X Y Z : Top} (f : W Y) (g : X Z) :
theorem Top.inducing_prod_map {W X Y Z : Top} {f : W X} {g : Y Z} (hf : inducing f) (hg : inducing g) :
theorem Top.embedding_prod_map {W X Y Z : Top} {f : W X} {g : Y Z} (hf : embedding f) (hg : embedding g) :
@[reducible]
def Top.pullback_fst {X Y Z : Top} (f : X Z) (g : Y Z) :
Top.of {p // f p.fst = g p.snd} X

The first projection from the pullback.

@[reducible]
def Top.pullback_snd {X Y Z : Top} (f : X Z) (g : Y Z) :
Top.of {p // f p.fst = g p.snd} Y

The second projection from the pullback.

def Top.pullback_cone {X Y Z : Top} (f : X Z) (g : Y Z) :

The explicit pullback cone of X, Y given by { p : X × Y // f p.1 = g p.2 }.

Equations
def Top.pullback_cone_is_limit {X Y Z : Top} (f : X Z) (g : Y Z) :

The constructed cone is a limit.

Equations
noncomputable def Top.pullback_iso_prod_subtype {X Y Z : Top} (f : X Z) (g : Y Z) :
Top.of {p // f p.fst = g p.snd}

The pullback of two maps can be identified as a subspace of X × Y.

Equations
@[simp]
theorem Top.pullback_iso_prod_subtype_inv_fst_assoc {X Y Z : Top} (f : X Z) (g : Y Z) {X' : Top} (f' : X X') :
@[simp]
theorem Top.pullback_iso_prod_subtype_inv_fst {X Y Z : Top} (f : X Z) (g : Y Z) :
@[simp]
theorem Top.pullback_iso_prod_subtype_inv_fst_apply {X Y Z : Top} (f : X Z) (g : Y Z) (x : {p // f p.fst = g p.snd}) :
@[simp]
theorem Top.pullback_iso_prod_subtype_inv_snd {X Y Z : Top} (f : X Z) (g : Y Z) :
@[simp]
theorem Top.pullback_iso_prod_subtype_inv_snd_assoc {X Y Z : Top} (f : X Z) (g : Y Z) {X' : Top} (f' : Y X') :
@[simp]
theorem Top.pullback_iso_prod_subtype_inv_snd_apply {X Y Z : Top} (f : X Z) (g : Y Z) (x : {p // f p.fst = g p.snd}) :
theorem Top.pullback_iso_prod_subtype_hom_fst {X Y Z : Top} (f : X Z) (g : Y Z) :
theorem Top.pullback_iso_prod_subtype_hom_snd {X Y Z : Top} (f : X Z) (g : Y Z) :
@[simp]
theorem Top.pullback_iso_prod_subtype_hom_apply {X Y Z : Top} {f : X Z} {g : Y Z} (x : ) :
theorem Top.range_pullback_to_prod {X Y Z : Top} (f : X Z) (g : Y Z) :
theorem Top.inducing_pullback_to_prod {X Y Z : Top} (f : X Z) (g : Y Z) :
theorem Top.embedding_pullback_to_prod {X Y Z : Top} (f : X Z) (g : Y Z) :
theorem Top.range_pullback_map {W X Y Z S T : Top} (f₁ : W S) (f₂ : X S) (g₁ : Y T) (g₂ : Z T) (i₁ : W Y) (i₂ : X Z) (i₃ : S T) [H₃ : category_theory.mono i₃] (eq₁ : f₁ i₃ = i₁ g₁) (eq₂ : f₂ i₃ = i₂ g₂) :
set.range g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) =

If the map S ⟶ T is mono, then there is a description of the image of W ×ₛ X ⟶ Y ×ₜ Z.

theorem Top.pullback_fst_range {X Y S : Top} (f : X S) (g : Y S) :
= {x : X | (y : Y), f x = g y}
theorem Top.pullback_snd_range {X Y S : Top} (f : X S) (g : Y S) :
= {y : Y | (x : X), f x = g y}
theorem Top.pullback_map_embedding_of_embeddings {W X Y Z S T : Top} (f₁ : W S) (f₂ : X S) (g₁ : Y T) (g₂ : Z T) {i₁ : W Y} {i₂ : X Z} (H₁ : embedding i₁) (H₂ : embedding i₂) (i₃ : S T) (eq₁ : f₁ i₃ = i₁ g₁) (eq₂ : f₂ i₃ = i₂ g₂) :
embedding g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

If there is a diagram where the morphisms W ⟶ Y and X ⟶ Z are embeddings, then the induced morphism W ×ₛ X ⟶ Y ×ₜ Z is also an embedding.

W ⟶ Y ↘ ↘ S ⟶ T ↗ ↗ X ⟶ Z

theorem Top.pullback_map_open_embedding_of_open_embeddings {W X Y Z S T : Top} (f₁ : W S) (f₂ : X S) (g₁ : Y T) (g₂ : Z T) {i₁ : W Y} {i₂ : X Z} (H₁ : open_embedding i₁) (H₂ : open_embedding i₂) (i₃ : S T) [H₃ : category_theory.mono i₃] (eq₁ : f₁ i₃ = i₁ g₁) (eq₂ : f₂ i₃ = i₂ g₂) :
open_embedding g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

If there is a diagram where the morphisms W ⟶ Y and X ⟶ Z are open embeddings, and S ⟶ T is mono, then the induced morphism W ×ₛ X ⟶ Y ×ₜ Z is also an open embedding. W ⟶ Y ↘ ↘ S ⟶ T ↗ ↗ X ⟶ Z

theorem Top.snd_embedding_of_left_embedding {X Y S : Top} {f : X S} (H : embedding f) (g : Y S) :
theorem Top.fst_embedding_of_right_embedding {X Y S : Top} (f : X S) {g : Y S} (H : embedding g) :
theorem Top.embedding_of_pullback_embeddings {X Y S : Top} {f : X S} {g : Y S} (H₁ : embedding f) (H₂ : embedding g) :
theorem Top.snd_open_embedding_of_left_open_embedding {X Y S : Top} {f : X S} (H : open_embedding f) (g : Y S) :
theorem Top.fst_open_embedding_of_right_open_embedding {X Y S : Top} (f : X S) {g : Y S} (H : open_embedding g) :
theorem Top.open_embedding_of_pullback_open_embeddings {X Y S : Top} {f : X S} {g : Y S} (H₁ : open_embedding f) (H₂ : open_embedding g) :

If X ⟶ S, Y ⟶ S are open embeddings, then so is X ×ₛ Y ⟶ S.

theorem Top.fst_iso_of_right_embedding_range_subset {X Y S : Top} (f : X S) {g : Y S} (hg : embedding g) (H : ) :
theorem Top.snd_iso_of_left_embedding_range_subset {X Y S : Top} {f : X S} (hf : embedding f) (g : Y S) (H : ) :
theorem Top.pullback_snd_image_fst_preimage {X Y Z : Top} (f : X Z) (g : Y Z) (U : set X) :
theorem Top.pullback_fst_image_snd_preimage {X Y Z : Top} (f : X Z) (g : Y Z) (U : set Y) :

The terminal object of Top is punit.

Equations
noncomputable def Top.terminal_iso_punit  :

The terminal object of Top is punit.

Equations

The initial object of Top is pempty.

Equations
noncomputable def Top.initial_iso_pempty  :

The initial object of Top is pempty.

Equations
@[protected]
def Top.binary_cofan (X Y : Top) :

The binary coproduct cofan in Top.

Equations

The constructed binary coproduct cofan in Top is the coproduct.

Equations
theorem Top.colimit_topology {J : Type v} (F : J Top) :
theorem Top.colimit_is_open_iff {J : Type v} (F : J Top) (U : set ) :
(j : J), is_open ⁻¹' U)
theorem Top.is_topological_basis_cofiltered_limit {J : Type v} (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 i U2 T i U1 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} [preorder J] [is_directed J (≤)] and F : Jᵒᵖ ⥤ Top.

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 category_theory.cofiltered_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.