mathlib3 documentation

topology.category.Top.limits.pullbacks

Pullbacks in the category of topological spaces. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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