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

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

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

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

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
@[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 ι) :
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') :
@[simp]
theorem Top.pi_iso_pi_inv_π {ι : Type v} (α : ι → Top) (i : ι) :
@[simp]
theorem Top.pi_iso_pi_inv_π_apply {ι : Type v} (α : ι → Top) (i : ι) (x : Π (i : ι), (α i)) :
@[simp]
theorem Top.pi_iso_pi_hom_apply {ι : Type v} (α : ι → Top) (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) :
(Top.sigma_cofan α).X = Top.of (Σ (i : ι), (α i))
@[simp]
theorem Top.sigma_cofan_ι_app {ι : Type v} (α : ι → Top) (X : category_theory.discrete ι) :

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') :
@[simp]
theorem Top.sigma_iso_sigma_hom_ι_apply {ι : Type v} (α : ι → Top) (i : ι) (x : (α i)) :
@[simp]
theorem Top.sigma_iso_sigma_inv_apply {ι : Type v} (α : ι → Top) (i : ι) (x : (α i)) :
@[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.

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

The constructed cone is a limit.

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

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

Equations
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₂) :

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) :
theorem Top.pullback_snd_range {X Y S : Top} (f : X S) (g : Y S) :
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

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

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

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 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} [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 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} [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
theorem Top.partial_sections.nonempty {J : Type u} [category_theory.small_category J] (F : J Top) [category_theory.is_cofiltered J] [h : ∀ (j : J), nonempty (F.obj j)] {G : finset J} (H : finset (finite_diagram_arrow G)) :
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)
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)) :

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

theorem nonempty_sections_of_fintype_cofiltered_system.init {J : Type u} [category_theory.small_category J] [category_theory.is_cofiltered J] (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} [category_theory.category J] [category_theory.is_cofiltered J] (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} [preorder J] [is_directed J has_le.le] (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.