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.

source
def Top.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) :
category_theory.limits.cone F

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
source
def Top.limit_cone_infi {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) :
category_theory.limits.cone F

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
source
def Top.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) :
category_theory.limits.is_limit (Top.limit_cone F)

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
source
def Top.limit_cone_infi_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) :
category_theory.limits.is_limit (Top.limit_cone_infi F)

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
source
@[protected, instance]
def Top.Top_has_limits_of_size  :
category_theory.limits.has_limits_of_size Top
source
@[protected, instance]
def Top.Top_has_limits  :
category_theory.limits.has_limits Top
source
@[protected, instance]
def Top.forget_preserves_limits_of_size  :
category_theory.limits.preserves_limits_of_size (category_theory.forget Top)
Equations
source
@[protected, instance]
def Top.forget_preserves_limits  :
category_theory.limits.preserves_limits (category_theory.forget Top)
Equations
source
def Top.colimit_cocone {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) :
category_theory.limits.cocone F

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
source
def Top.colimit_cocone_is_colimit {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) :
category_theory.limits.is_colimit (Top.colimit_cocone F)

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
source
@[protected, instance]
def Top.Top_has_colimits_of_size  :
category_theory.limits.has_colimits_of_size Top
source
@[protected, instance]
def Top.Top_has_colimits  :
category_theory.limits.has_colimits Top
source
@[protected, instance]
def Top.forget_preserves_colimits_of_size  :
category_theory.limits.preserves_colimits_of_size (category_theory.forget Top)
Equations
source
@[protected, instance]
def Top.forget_preserves_colimits  :
category_theory.limits.preserves_colimits (category_theory.forget Top)
Equations
source
@[reducible]
def Top.pi_π {ι : Type v} (α : ι → Top) (i : ι) :
Top.of (Π (i : ι), ↥(α i)) ⟶ α i

The projection from the product as a bundled continous map.

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

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

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

The constructed fan is indeed a limit

Equations
source
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
source
@[simp]
theorem Top.pi_iso_pi_inv_π_assoc {ι : Type v} (α : ι → Top) (i : ι) {X' : Top} (f' : α i ⟶ X') :
(Top.pi_iso_pi α).inv ≫ category_theory.limits.pi.π α i ≫ f' = Top.pi_π α i ≫ f'
source
@[simp]
theorem Top.pi_iso_pi_inv_π {ι : Type v} (α : ι → Top) (i : ι) :
(Top.pi_iso_pi α).inv ≫ category_theory.limits.pi.π α i = Top.pi_π α i
source
@[simp]
theorem Top.pi_iso_pi_inv_π_apply {ι : Type v} (α : ι → Top) (i : ι) (x : Π (i : ι), ↥(α i)) :
⇑(category_theory.limits.pi.π α i) (⇑((Top.pi_iso_pi α).inv) x) = x i
source
@[simp]
theorem Top.pi_iso_pi_hom_apply {ι : Type v} (α : ι → Top) (i : ι) (x : ↥∏ α) :
⇑((Top.pi_iso_pi α).hom) x i = ⇑(category_theory.limits.pi.π α i) x
source
@[reducible]
def Top.sigma_ι {ι : Type v} (α : ι → Top) (i : ι) :
α i ⟶ Top.of (Σ (i : ι), ↥(α i))

The inclusion to the coproduct as a bundled continous map.

source
def Top.sigma_cofan {ι : Type v} (α : ι → Top) :
category_theory.limits.cofan α

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

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

The constructed cofan is indeed a colimit

Equations
source
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
source
@[simp]
theorem Top.sigma_iso_sigma_hom_ι {ι : Type v} (α : ι → Top) (i : ι) :
category_theory.limits.sigma.ι α i ≫ (Top.sigma_iso_sigma α).hom = Top.sigma_ι α i
source
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_assoc {ι : Type v} (α : ι → Top) (i : ι) {X' : Top} (f' : Top.of (Σ (i : ι), ↥(α i)) ⟶ X') :
category_theory.limits.sigma.ι α i ≫ (Top.sigma_iso_sigma α).hom ≫ f' = Top.sigma_ι α i ≫ f'
source
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_apply {ι : Type v} (α : ι → Top) (i : ι) (x : ↥(α i)) :
⇑((Top.sigma_iso_sigma α).hom) (⇑(category_theory.limits.sigma.ι α i) x) = ⟨i, x⟩
source
@[simp]
theorem Top.sigma_iso_sigma_inv_apply {ι : Type v} (α : ι → Top) (i : ι) (x : ↥(α i)) :
⇑((Top.sigma_iso_sigma α).inv) ⟨i, x⟩ = ⇑(category_theory.limits.sigma.ι α i) x
source
theorem Top.induced_of_is_limit {J : Type v} [category_theory.small_category J] {F : J ⥤ Top} (C : category_theory.limits.cone F) (hC : category_theory.limits.is_limit C) :
C.X.topological_space = ⨅ (j : J), topological_space.induced ⇑(C.π.app j) (F.obj j).topological_space
source
theorem Top.limit_topology {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) :
(category_theory.limits.limit F).topological_space = ⨅ (j : J), topological_space.induced ⇑(category_theory.limits.limit.π F j) (F.obj j).topological_space
source
@[reducible]
def Top.prod_fst {X Y : Top} :
Top.of (↥X × ↥Y) ⟶ X

The first projection from the product.

source
@[reducible]
def Top.prod_snd {X Y : Top} :
Top.of (↥X × ↥Y) ⟶ Y

The second projection from the product.

source
def Top.prod_binary_fan (X Y : Top) :
category_theory.limits.binary_fan X Y

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

Equations
source
def Top.prod_binary_fan_is_limit (X Y : Top) :
category_theory.limits.is_limit (X.prod_binary_fan Y)

The constructed binary fan is indeed a limit

Equations
source
noncomputable def Top.prod_iso_prod (X Y : Top) :
X ⨯ Y ≅ Top.of (↥X × ↥Y)

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

Equations
source
@[simp]
theorem Top.prod_iso_prod_hom_fst (X Y : Top) :
(X.prod_iso_prod Y).hom ≫ Top.prod_fst = category_theory.limits.prod.fst
source
@[simp]
theorem Top.prod_iso_prod_hom_fst_assoc (X Y : Top) {X' : Top} (f' : X ⟶ X') :
(X.prod_iso_prod Y).hom ≫ Top.prod_fst ≫ f' = category_theory.limits.prod.fst ≫ f'
source
@[simp]
theorem Top.prod_iso_prod_hom_snd (X Y : Top) :
(X.prod_iso_prod Y).hom ≫ Top.prod_snd = category_theory.limits.prod.snd
source
@[simp]
theorem Top.prod_iso_prod_hom_snd_assoc (X Y : Top) {X' : Top} (f' : Y ⟶ X') :
(X.prod_iso_prod Y).hom ≫ Top.prod_snd ≫ f' = category_theory.limits.prod.snd ≫ f'
source
@[simp]
theorem Top.prod_iso_prod_hom_apply {X Y : Top} (x : ↥(X ⨯ Y)) :
⇑((X.prod_iso_prod Y).hom) x = (⇑category_theory.limits.prod.fst x, ⇑category_theory.limits.prod.snd x)
source
@[simp]
theorem Top.prod_iso_prod_inv_fst_apply (X Y : Top) (x : ↥(Top.of (↥X × ↥Y))) :
⇑category_theory.limits.prod.fst (⇑((X.prod_iso_prod Y).inv) x) = ⇑Top.prod_fst x
source
@[simp]
theorem Top.prod_iso_prod_inv_fst_assoc (X Y : Top) {X' : Top} (f' : X ⟶ X') :
(X.prod_iso_prod Y).inv ≫ category_theory.limits.prod.fst ≫ f' = Top.prod_fst ≫ f'
source
@[simp]
theorem Top.prod_iso_prod_inv_fst (X Y : Top) :
(X.prod_iso_prod Y).inv ≫ category_theory.limits.prod.fst = Top.prod_fst
source
@[simp]
theorem Top.prod_iso_prod_inv_snd (X Y : Top) :
(X.prod_iso_prod Y).inv ≫ category_theory.limits.prod.snd = Top.prod_snd
source
@[simp]
theorem Top.prod_iso_prod_inv_snd_apply (X Y : Top) (x : ↥(Top.of (↥X × ↥Y))) :
⇑category_theory.limits.prod.snd (⇑((X.prod_iso_prod Y).inv) x) = ⇑Top.prod_snd x
source
@[simp]
theorem Top.prod_iso_prod_inv_snd_assoc (X Y : Top) {X' : Top} (f' : Y ⟶ X') :
(X.prod_iso_prod Y).inv ≫ category_theory.limits.prod.snd ≫ f' = Top.prod_snd ≫ f'
source
theorem Top.prod_topology {X Y : Top} :
(X ⨯ Y).topological_space = topological_space.induced ⇑category_theory.limits.prod.fst X.topological_space ⊓ topological_space.induced ⇑category_theory.limits.prod.snd Y.topological_space
source
theorem Top.range_prod_map {W X Y Z : Top} (f : W ⟶ Y) (g : X ⟶ Z) :
set.range ⇑(category_theory.limits.prod.map f g) = ⇑category_theory.limits.prod.fst ⁻¹' set.range ⇑f ∩ ⇑category_theory.limits.prod.snd ⁻¹' set.range ⇑g
source
theorem Top.inducing_prod_map {W X Y Z : Top} {f : W ⟶ X} {g : Y ⟶ Z} (hf : inducing ⇑f) (hg : inducing ⇑g) :
inducing ⇑(category_theory.limits.prod.map f g)
source
theorem Top.embedding_prod_map {W X Y Z : Top} {f : W ⟶ X} {g : Y ⟶ Z} (hf : embedding ⇑f) (hg : embedding ⇑g) :
embedding ⇑(category_theory.limits.prod.map f g)
source
@[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.

source
@[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.

source
def Top.pullback_cone {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
category_theory.limits.pullback_cone f g

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

Equations
source
def Top.pullback_cone_is_limit {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
category_theory.limits.is_limit (Top.pullback_cone f g)

The constructed cone is a limit.

Equations
source
noncomputable def Top.pullback_iso_prod_subtype {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
category_theory.limits.pullback f g ≅ Top.of {p // ⇑f p.fst = ⇑g p.snd}

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

Equations
source
@[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') :
(Top.pullback_iso_prod_subtype f g).inv ≫ category_theory.limits.pullback.fst ≫ f' = Top.pullback_fst f g ≫ f'
source
@[simp]
theorem Top.pullback_iso_prod_subtype_inv_fst {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
(Top.pullback_iso_prod_subtype f g).inv ≫ category_theory.limits.pullback.fst = Top.pullback_fst f g
source
@[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}) :
⇑category_theory.limits.pullback.fst (⇑((Top.pullback_iso_prod_subtype f g).inv) x) = ↑x.fst
source
@[simp]
theorem Top.pullback_iso_prod_subtype_inv_snd {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
(Top.pullback_iso_prod_subtype f g).inv ≫ category_theory.limits.pullback.snd = Top.pullback_snd f g
source
@[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') :
(Top.pullback_iso_prod_subtype f g).inv ≫ category_theory.limits.pullback.snd ≫ f' = Top.pullback_snd f g ≫ f'
source
@[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}) :
⇑category_theory.limits.pullback.snd (⇑((Top.pullback_iso_prod_subtype f g).inv) x) = ↑x.snd
source
theorem Top.pullback_iso_prod_subtype_hom_fst {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
(Top.pullback_iso_prod_subtype f g).hom ≫ Top.pullback_fst f g = category_theory.limits.pullback.fst
source
theorem Top.pullback_iso_prod_subtype_hom_snd {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
(Top.pullback_iso_prod_subtype f g).hom ≫ Top.pullback_snd f g = category_theory.limits.pullback.snd
source
@[simp]
theorem Top.pullback_iso_prod_subtype_hom_apply {X Y Z : Top} {f : X ⟶ Z} {g : Y ⟶ Z} (x : ↥(category_theory.limits.pullback f g)) :
⇑((Top.pullback_iso_prod_subtype f g).hom) x = ⟨(⇑category_theory.limits.pullback.fst x, ⇑category_theory.limits.pullback.snd x), _⟩
source
theorem Top.pullback_topology {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.pullback f g).topological_space = topological_space.induced ⇑category_theory.limits.pullback.fst X.topological_space ⊓ topological_space.induced ⇑category_theory.limits.pullback.snd Y.topological_space
source
theorem Top.range_pullback_to_prod {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
set.range ⇑(category_theory.limits.prod.lift category_theory.limits.pullback.fst category_theory.limits.pullback.snd) = {x : ↥(X ⨯ Y) | ⇑(category_theory.limits.prod.fst ≫ f) x = ⇑(category_theory.limits.prod.snd ≫ g) x}
source
theorem Top.inducing_pullback_to_prod {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
inducing ⇑(category_theory.limits.prod.lift category_theory.limits.pullback.fst category_theory.limits.pullback.snd)
source
theorem Top.embedding_pullback_to_prod {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) :
embedding ⇑(category_theory.limits.prod.lift category_theory.limits.pullback.fst category_theory.limits.pullback.snd)
source
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 ⇑(category_theory.limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) = ⇑category_theory.limits.pullback.fst ⁻¹' set.range ⇑i₁ ∩ ⇑category_theory.limits.pullback.snd ⁻¹' set.range ⇑i₂

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

source
theorem Top.pullback_fst_range {X Y S : Top} (f : X ⟶ S) (g : Y ⟶ S) :
set.range ⇑category_theory.limits.pullback.fst = {x : ↥X | ∃ (y : ↥Y), ⇑f x = ⇑g y}
source
theorem Top.pullback_snd_range {X Y S : Top} (f : X ⟶ S) (g : Y ⟶ S) :
set.range ⇑category_theory.limits.pullback.snd = {y : ↥Y | ∃ (x : ↥X), ⇑f x = ⇑g y}
source
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 ⇑(category_theory.limits.pullback.map f₁ f₂ 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

source
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 ⇑(category_theory.limits.pullback.map f₁ f₂ 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

source
theorem Top.snd_embedding_of_left_embedding {X Y S : Top} {f : X ⟶ S} (H : embedding ⇑f) (g : Y ⟶ S) :
embedding ⇑category_theory.limits.pullback.snd
source
theorem Top.fst_embedding_of_right_embedding {X Y S : Top} (f : X ⟶ S) {g : Y ⟶ S} (H : embedding ⇑g) :
embedding ⇑category_theory.limits.pullback.fst
source
theorem Top.embedding_of_pullback_embeddings {X Y S : Top} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : embedding ⇑f) (H₂ : embedding ⇑g) :
embedding ⇑(category_theory.limits.limit.π (category_theory.limits.cospan f g) category_theory.limits.walking_cospan.one)
source
theorem Top.snd_open_embedding_of_left_open_embedding {X Y S : Top} {f : X ⟶ S} (H : open_embedding ⇑f) (g : Y ⟶ S) :
open_embedding ⇑category_theory.limits.pullback.snd
source
theorem Top.fst_open_embedding_of_right_open_embedding {X Y S : Top} (f : X ⟶ S) {g : Y ⟶ S} (H : open_embedding ⇑g) :
open_embedding ⇑category_theory.limits.pullback.fst
source
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) :
open_embedding ⇑(category_theory.limits.limit.π (category_theory.limits.cospan f g) category_theory.limits.walking_cospan.one)

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

source
theorem Top.fst_iso_of_right_embedding_range_subset {X Y S : Top} (f : X ⟶ S) {g : Y ⟶ S} (hg : embedding ⇑g) (H : set.range ⇑f ⊆ set.range ⇑g) :
category_theory.is_iso category_theory.limits.pullback.fst
source
theorem Top.snd_iso_of_left_embedding_range_subset {X Y S : Top} {f : X ⟶ S} (hf : embedding ⇑f) (g : Y ⟶ S) (H : set.range ⇑g ⊆ set.range ⇑f) :
category_theory.is_iso category_theory.limits.pullback.snd
source
theorem Top.pullback_snd_image_fst_preimage {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) (U : set ↥X) :
⇑category_theory.limits.pullback.snd '' (⇑category_theory.limits.pullback.fst ⁻¹' U) = ⇑g ⁻¹' (⇑f '' U)
source
theorem Top.pullback_fst_image_snd_preimage {X Y Z : Top} (f : X ⟶ Z) (g : Y ⟶ Z) (U : set ↥Y) :
⇑category_theory.limits.pullback.fst '' (⇑category_theory.limits.pullback.snd ⁻¹' U) = ⇑f ⁻¹' (⇑g '' U)
source
def Top.is_terminal_punit  :
category_theory.limits.is_terminal (Top.of punit)

The terminal object of Top is punit.

Equations
source
noncomputable def Top.terminal_iso_punit  :
⊤_ Top ≅ Top.of punit

The terminal object of Top is punit.

Equations
source
def Top.is_initial_pempty  :
category_theory.limits.is_initial (Top.of pempty)

The initial object of Top is pempty.

Equations
source
noncomputable def Top.initial_iso_pempty  :
⊥_ Top ≅ Top.of pempty

The initial object of Top is pempty.

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

The binary coproduct cofan in Top.

Equations
source
def Top.binary_cofan_is_colimit (X Y : Top) :
category_theory.limits.is_colimit (X.binary_cofan Y)

The constructed binary coproduct cofan in Top is the coproduct.

Equations
source
theorem Top.binary_cofan_is_colimit_iff {X Y : Top} (c : category_theory.limits.binary_cofan X Y) :
nonempty (category_theory.limits.is_colimit c) ↔ open_embedding ⇑(c.inl) ∧ open_embedding ⇑(c.inr) ∧ is_compl (set.range ⇑(c.inl)) (set.range ⇑(c.inr))
source
theorem Top.coinduced_of_is_colimit {J : Type v} [category_theory.small_category J] {F : J ⥤ Top} (c : category_theory.limits.cocone F) (hc : category_theory.limits.is_colimit c) :
c.X.topological_space = ⨆ (j : J), topological_space.coinduced ⇑(c.ι.app j) (F.obj j).topological_space
source
theorem Top.colimit_topology {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) :
(category_theory.limits.colimit F).topological_space = ⨆ (j : J), topological_space.coinduced ⇑(category_theory.limits.colimit.ι F j) (F.obj j).topological_space
source
theorem Top.colimit_is_open_iff {J : Type v} [category_theory.small_category J] (F : J ⥤ Top) (U : set ↥(category_theory.limits.colimit F)) :
is_open U ↔ ∀ (j : J), is_open (⇑(category_theory.limits.colimit.ι F j) ⁻¹' U)
source
theorem Top.coequalizer_is_open_iff (F : category_theory.limits.walking_parallel_pair ⥤ Top) (U : set ↥(category_theory.limits.colimit F)) :
is_open U ↔ is_open (⇑(category_theory.limits.colimit.ι F category_theory.limits.walking_parallel_pair.one) ⁻¹' U)
source
theorem Top.is_topological_basis_cofiltered_limit {J : Type v} [category_theory.small_category J] [category_theory.is_cofiltered J] (F : J ⥤ Top) (C : category_theory.limits.cone F) (hC : category_theory.limits.is_limit C) (T : Π (j : J), set (set ↥(F.obj j))) (hT : ∀ (j : J), topological_space.is_topological_basis (T 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.)

source
def Top.partial_sections {J : Type u} [category_theory.small_category J] (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
source
theorem Top.partial_sections.nonempty {J : Type u} [category_theory.small_category J] (F : J ⥤ Top) [category_theory.is_cofiltered_or_empty J] [h : ∀ (j : J), nonempty ↥(F.obj j)] {G : finset J} (H : finset (finite_diagram_arrow G)) :
(Top.partial_sections F H).nonempty
source
theorem Top.partial_sections.directed {J : Type u} [category_theory.small_category J] (F : J ⥤ Top) :
directed superset (λ (G : finite_diagram J), Top.partial_sections F G.snd)
source
theorem Top.partial_sections.closed {J : Type u} [category_theory.small_category J] (F : J ⥤ Top) [∀ (j : J), t2_space ↥(F.obj j)] {G : finset J} (H : finset (finite_diagram_arrow G)) :
is_closed (Top.partial_sections F H)
source
theorem Top.nonempty_limit_cone_of_compact_t2_cofiltered_system {J : Type u} [category_theory.small_category J] (F : J ⥤ Top) [category_theory.is_cofiltered_or_empty J] [∀ (j : J), nonempty ↥(F.obj j)] [∀ (j : J), compact_space ↥(F.obj j)] [∀ (j : J), t2_space ↥(F.obj j)] :
nonempty ↥((Top.limit_cone F).X)

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