# Pullbacks and pushouts in the category of topological spaces #

@[reducible, inline]
abbrev TopCat.pullbackFst {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
TopCat.of { p : X × Y // f p.1 = g p.2 } X

The first projection from the pullback.

Equations
• = { toFun := Prod.fst Subtype.val, continuous_toFun := }
Instances For
theorem TopCat.pullbackFst_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (x : (TopCat.of { p : X × Y // f p.1 = g p.2 })) :
() x = (x).1
@[reducible, inline]
abbrev TopCat.pullbackSnd {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
TopCat.of { p : X × Y // f p.1 = g p.2 } Y

The second projection from the pullback.

Equations
• = { toFun := Prod.snd Subtype.val, continuous_toFun := }
Instances For
theorem TopCat.pullbackSnd_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (x : (TopCat.of { p : X × Y // f p.1 = g p.2 })) :
() x = (x).2
def TopCat.pullbackCone {X : TopCat} {Y : TopCat} {Z : TopCat} (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
Instances For
def TopCat.pullbackConeIsLimit {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :

The constructed cone is a limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def TopCat.pullbackIsoProdSubtype {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
TopCat.of { p : X × Y // f p.1 = g p.2 }

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

Equations
• = .conePointUniqueUpToIso
Instances For
@[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 .inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) =
@[simp]
theorem TopCat.pullbackIsoProdSubtype_inv_fst {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
CategoryTheory.CategoryStruct.comp .inv CategoryTheory.Limits.pullback.fst =
theorem TopCat.pullbackIsoProdSubtype_inv_fst_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (x : { p : X × Y // f p.1 = g p.2 }) :
CategoryTheory.Limits.pullback.fst (.inv x) = (x).1
@[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 .inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) =
@[simp]
theorem TopCat.pullbackIsoProdSubtype_inv_snd {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
CategoryTheory.CategoryStruct.comp .inv CategoryTheory.Limits.pullback.snd =
theorem TopCat.pullbackIsoProdSubtype_inv_snd_apply {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) (x : { p : X × Y // f p.1 = g p.2 }) :
CategoryTheory.Limits.pullback.snd (.inv x) = (x).2
theorem TopCat.pullbackIsoProdSubtype_hom_fst {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
= CategoryTheory.Limits.pullback.fst
theorem TopCat.pullbackIsoProdSubtype_hom_snd {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
= CategoryTheory.Limits.pullback.snd
theorem TopCat.pullbackIsoProdSubtype_hom_apply {X : TopCat} {Y : TopCat} {Z : TopCat} {f : X Z} {g : Y Z} (x : CategoryTheory.ConcreteCategory.forget.obj ) :
.hom x = (CategoryTheory.Limits.pullback.fst x, CategoryTheory.Limits.pullback.snd x),
theorem TopCat.pullback_topology {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X Z) (g : Y Z) :
.str = TopologicalSpace.induced (CategoryTheory.Limits.pullback.fst) X.str TopologicalSpace.induced (CategoryTheory.Limits.pullback.snd) Y.str
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 : (X Y) | (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f) x = (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g) x}
noncomputable def TopCat.pullbackHomeoPreimage {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] (f : XZ) (hf : ) (g : YZ) (hg : ) :
{ p : X × Y // f p.1 = g p.2 } ≃ₜ (f ⁻¹' )

The pullback along an embedding is (isomorphic to) the preimage.

Equations
• One or more equations did not get rendered due to their size.
Instances For
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)
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)
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₃ : ] (eq₁ : ) (eq₂ : ) :
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.

theorem TopCat.pullback_fst_range {X : TopCat} {Y : TopCat} {S : TopCat} (f : X S) (g : Y S) :
Set.range CategoryTheory.Limits.pullback.fst = {x : X | ∃ (y : Y), f x = g y}
theorem TopCat.pullback_snd_range {X : TopCat} {Y : TopCat} {S : TopCat} (f : X S) (g : Y S) :
Set.range CategoryTheory.Limits.pullback.snd = {y : Y | ∃ (x : X), f x = g y}
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₁ : ) (eq₂ : ) :
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

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₁ : ) (H₂ : ) (i₃ : S T) [H₃ : ] (eq₁ : ) (eq₂ : ) :
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

theorem TopCat.snd_embedding_of_left_embedding {X : TopCat} {Y : TopCat} {S : TopCat} {f : X S} (H : ) (g : Y S) :
Embedding CategoryTheory.Limits.pullback.snd
theorem TopCat.fst_embedding_of_right_embedding {X : TopCat} {Y : TopCat} {S : TopCat} (f : X S) {g : Y S} (H : ) :
Embedding CategoryTheory.Limits.pullback.fst
theorem TopCat.embedding_of_pullback_embeddings {X : TopCat} {Y : TopCat} {S : TopCat} {f : X S} {g : Y S} (H₁ : ) (H₂ : ) :
theorem TopCat.snd_openEmbedding_of_left_openEmbedding {X : TopCat} {Y : TopCat} {S : TopCat} {f : X S} (H : ) (g : Y S) :
OpenEmbedding CategoryTheory.Limits.pullback.snd
theorem TopCat.fst_openEmbedding_of_right_openEmbedding {X : TopCat} {Y : TopCat} {S : TopCat} (f : X S) {g : Y S} (H : ) :
OpenEmbedding CategoryTheory.Limits.pullback.fst
theorem TopCat.openEmbedding_of_pullback_open_embeddings {X : TopCat} {Y : TopCat} {S : TopCat} {f : X S} {g : Y S} (H₁ : ) (H₂ : ) :

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

theorem TopCat.fst_iso_of_right_embedding_range_subset {X : TopCat} {Y : TopCat} {S : TopCat} (f : X S) {g : Y S} (hg : ) (H : ) :
CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst
theorem TopCat.snd_iso_of_left_embedding_range_subset {X : TopCat} {Y : TopCat} {S : TopCat} {f : X S} (hf : ) (g : Y S) (H : ) :
CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd
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)
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)
theorem TopCat.coinduced_of_isColimit {J : Type v} {F : } (c : ) (hc : ) :
c.pt.str = ⨆ (j : J), TopologicalSpace.coinduced ((c.app j)) (F.obj j).str
theorem TopCat.colimit_topology {J : Type v} (F : ) :
.str = ⨆ (j : J), TopologicalSpace.coinduced () (F.obj j).str
theorem TopCat.colimit_isOpen_iff {J : Type v} (F : ) (U : ) :
∀ (j : J), IsOpen ()