Pullbacks and pushouts in the category of topological spaces #

@[inline, reducible]

abbrev TopCat.pullbackFst {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

TopCat.of { p // ↑f p.fst = ↑g p.snd } ⟶ X

The first projection from the pullback.

Instances For

@[simp]

theorem TopCat.pullbackFst_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (x : (CategoryTheory.forget TopCat).obj (TopCat.of { p // ↑f p.fst = ↑g p.snd })) :

↑(TopCat.pullbackFst f g) x = (↑x).fst

source

@[inline, reducible]

abbrev TopCat.pullbackSnd {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

TopCat.of { p // ↑f p.fst = ↑g p.snd } ⟶ Y

The second projection from the pullback.

Instances For

source

@[simp]

theorem TopCat.pullbackSnd_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (x : (CategoryTheory.forget TopCat).obj (TopCat.of { p // ↑f p.fst = ↑g p.snd })) :

↑(TopCat.pullbackSnd f g) x = (↑x).snd

source

def TopCat.pullbackCone {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.Limits.PullbackCone f g

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

Instances For

source

def TopCat.pullbackConeIsLimit {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.Limits.IsLimit (TopCat.pullbackCone f g)

The constructed cone is a limit.

Instances For

source

def TopCat.pullbackIsoProdSubtype {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.Limits.pullback f g ≅ TopCat.of { p // ↑f p.fst = ↑g p.snd }

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

Instances For

source

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_fst_assoc {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) {Z : TopCat} (h : X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp (TopCat.pullbackFst f g) h

source

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_fst {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).inv CategoryTheory.Limits.pullback.fst = TopCat.pullbackFst f g

source

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_fst_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (x : { p // ↑f p.fst = ↑g p.snd }) :

↑CategoryTheory.Limits.pullback.fst (↑(TopCat.pullbackIsoProdSubtype f g).inv x) = (↑x).fst

source

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_snd_assoc {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) {Z : TopCat} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp (TopCat.pullbackSnd f g) h

source

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_snd {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).inv CategoryTheory.Limits.pullback.snd = TopCat.pullbackSnd f g

source

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_snd_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (x : { p // ↑f p.fst = ↑g p.snd }) :

↑CategoryTheory.Limits.pullback.snd (↑(TopCat.pullbackIsoProdSubtype f g).inv x) = (↑x).snd

source

theorem TopCat.pullbackIsoProdSubtype_hom_fst {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).hom (TopCat.pullbackFst f g) = CategoryTheory.Limits.pullback.fst

source

theorem TopCat.pullbackIsoProdSubtype_hom_snd {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (TopCat.pullbackIsoProdSubtype f g).hom (TopCat.pullbackSnd f g) = CategoryTheory.Limits.pullback.snd

source

@[simp]

theorem TopCat.pullbackIsoProdSubtype_hom_apply {X : TopCat} {Y : TopCat} {Z : TopCat} {f : X ⟶ Z} {g : Y ⟶ Z} (x : CategoryTheory.ConcreteCategory.forget.obj (CategoryTheory.Limits.pullback f g)) :

↑(TopCat.pullbackIsoProdSubtype f g).hom x = { val := (↑CategoryTheory.Limits.pullback.fst x, ↑CategoryTheory.Limits.pullback.snd x), property := (_ : ↑f (↑CategoryTheory.Limits.pullback.fst x, ↑CategoryTheory.Limits.pullback.snd x).fst = ↑g (↑CategoryTheory.Limits.pullback.fst x, ↑CategoryTheory.Limits.pullback.snd x).snd) }

source

theorem TopCat.pullback_topology {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

(CategoryTheory.Limits.pullback f g).str = TopologicalSpace.induced (↑CategoryTheory.Limits.pullback.fst) X.str ⊓ TopologicalSpace.induced (↑CategoryTheory.Limits.pullback.snd) Y.str

source

theorem TopCat.range_pullback_to_prod {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

Set.range ↑(CategoryTheory.Limits.prod.lift CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) = {x | ↑(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f) x = ↑(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g) x}

source

theorem TopCat.inducing_pullback_to_prod {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

Inducing ↑(CategoryTheory.Limits.prod.lift CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)

source

theorem TopCat.embedding_pullback_to_prod {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

Embedding ↑(CategoryTheory.Limits.prod.lift CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)

source

theorem TopCat.range_pullback_map {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {S : TopCat} {T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) [H₃ : CategoryTheory.Mono i₃] (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) :

Set.range ↑(CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) = ↑CategoryTheory.Limits.pullback.fst ⁻¹' Set.range ↑i₁ ∩ ↑CategoryTheory.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 TopCat.pullback_fst_range {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) :

Set.range ↑CategoryTheory.Limits.pullback.fst = {x | ∃ y, ↑f x = ↑g y}

source

theorem TopCat.pullback_snd_range {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) :

Set.range ↑CategoryTheory.Limits.pullback.snd = {y | ∃ x, ↑f x = ↑g y}

source

theorem TopCat.pullback_map_embedding_of_embeddings {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {S : TopCat} {T : TopCat} (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₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) :

Embedding ↑(CategoryTheory.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 TopCat.pullback_map_openEmbedding_of_open_embeddings {W : TopCat} {X : TopCat} {Y : TopCat} {Z : TopCat} {S : TopCat} {T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : OpenEmbedding ↑i₁) (H₂ : OpenEmbedding ↑i₂) (i₃ : S ⟶ T) [H₃ : CategoryTheory.Mono i₃] (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) :

OpenEmbedding ↑(CategoryTheory.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 TopCat.snd_embedding_of_left_embedding {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} (H : Embedding ↑f) (g : Y ⟶ S) :

Embedding ↑CategoryTheory.Limits.pullback.snd

source

theorem TopCat.fst_embedding_of_right_embedding {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : Embedding ↑g) :

Embedding ↑CategoryTheory.Limits.pullback.fst

source

theorem TopCat.embedding_of_pullback_embeddings {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : Embedding ↑f) (H₂ : Embedding ↑g) :

Embedding ↑(CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)

source

theorem TopCat.snd_openEmbedding_of_left_openEmbedding {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} (H : OpenEmbedding ↑f) (g : Y ⟶ S) :

OpenEmbedding ↑CategoryTheory.Limits.pullback.snd

source

theorem TopCat.fst_openEmbedding_of_right_openEmbedding {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : OpenEmbedding ↑g) :

OpenEmbedding ↑CategoryTheory.Limits.pullback.fst

source

theorem TopCat.openEmbedding_of_pullback_open_embeddings {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : OpenEmbedding ↑f) (H₂ : OpenEmbedding ↑g) :

OpenEmbedding ↑(CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)

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

source

theorem TopCat.fst_iso_of_right_embedding_range_subset {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (hg : Embedding ↑g) (H : Set.range ↑f ⊆ Set.range ↑g) :

CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst

source

theorem TopCat.snd_iso_of_left_embedding_range_subset {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} (hf : Embedding ↑f) (g : Y ⟶ S) (H : Set.range ↑g ⊆ Set.range ↑f) :

CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd

source

theorem TopCat.pullback_snd_image_fst_preimage {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set ↑X) :

↑CategoryTheory.Limits.pullback.snd '' (↑CategoryTheory.Limits.pullback.fst ⁻¹' U) = ↑g ⁻¹' (↑f '' U)

source

theorem TopCat.pullback_fst_image_snd_preimage {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set ↑Y) :

↑CategoryTheory.Limits.pullback.fst '' (↑CategoryTheory.Limits.pullback.snd ⁻¹' U) = ↑f ⁻¹' (↑g '' U)

source

theorem TopCat.coinduced_of_isColimit {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TopCatMax} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) :

c.pt.str = ⨆ (j : J), TopologicalSpace.coinduced (↑(c.ι.app j)) (F.obj j).str

source

theorem TopCat.colimit_topology {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) :

(CategoryTheory.Limits.colimit F).str = ⨆ (j : J), TopologicalSpace.coinduced (↑(CategoryTheory.Limits.colimit.ι F j)) (F.obj j).str

source

theorem TopCat.colimit_isOpen_iff {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCatMax) (U : Set ↑(CategoryTheory.Limits.colimit F)) :

IsOpen U ↔ ∀ (j : J), IsOpen (↑(CategoryTheory.Limits.colimit.ι F j) ⁻¹' U)

source

theorem TopCat.coequalizer_isOpen_iff (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair TopCat) (U : Set ↑(CategoryTheory.Limits.colimit F)) :

IsOpen U ↔ IsOpen (↑(CategoryTheory.Limits.colimit.ι F CategoryTheory.Limits.WalkingParallelPair.one) ⁻¹' U)