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

• TopCat.pullbackFst f g = { toFun := Prod.fst ∘ Subtype.val, continuous_toFun := ⋯ }

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 })) : (TopCat.pullbackFst f g) 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

• TopCat.pullbackSnd f g = { toFun := Prod.snd ∘ Subtype.val, continuous_toFun := ⋯ }

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 })) : (TopCat.pullbackSnd f g) x = (↑x).2

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

Equations

• TopCat.pullbackCone f g = CategoryTheory.Limits.PullbackCone.mk (TopCat.pullbackFst f g) (TopCat.pullbackSnd f g) ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

def TopCat.pullbackIsoProdSubtype {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.pullback f g ≅ 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

• TopCat.pullbackIsoProdSubtype f g = (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.cospan f g)).conePointUniqueUpToIso (TopCat.pullbackConeIsLimit f g)

@[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 f g) h) = CategoryTheory.CategoryStruct.comp (TopCat.pullbackFst f g) h

@[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 f g) = TopCat.pullbackFst f g

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 f g) ((TopCat.pullbackIsoProdSubtype f g).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 (TopCat.pullbackIsoProdSubtype f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp (TopCat.pullbackSnd f g) h

@[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 f g) = TopCat.pullbackSnd f g

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 f g) ((TopCat.pullbackIsoProdSubtype f g).inv x) = (↑x).2

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

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

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 = ⟨((CategoryTheory.Limits.pullback.fst f g) x, (CategoryTheory.Limits.pullback.snd f g) x), ⋯⟩

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 f g)) X.str ⊓ TopologicalSpace.induced (⇑(CategoryTheory.Limits.pullback.snd f g)) 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 f g) (CategoryTheory.Limits.pullback.snd f g)) = {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} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : X → Z) (hf : Continuous f) (g : Y → Z) (hg : Embedding g) : { p : X × Y // f p.1 = g p.2 } ≃ₜ ↑(f ⁻¹' Set.range g)

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

Equations

• One or more equations did not get rendered due to their size.

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 f g) (CategoryTheory.Limits.pullback.snd f g))

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 f g) (CategoryTheory.Limits.pullback.snd f g))

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 g₁ g₂) ⁻¹' Set.range ⇑i₁ ∩ ⇑(CategoryTheory.Limits.pullback.snd g₁ g₂) ⁻¹' 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 f g) = {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 f g) = {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₁ : 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

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

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

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

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)

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

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

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.

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

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

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 f g) '' (⇑(CategoryTheory.Limits.pullback.fst f g) ⁻¹' 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 f g) '' (⇑(CategoryTheory.Limits.pullback.snd f g) ⁻¹' U) = ⇑f ⁻¹' (⇑g '' U)

theorem TopCat.coinduced_of_isColimit {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit c) : c.pt.str = ⨆ (j : J), TopologicalSpace.coinduced (⇑(c.ι.app j)) (F.obj j).str

theorem TopCat.colimit_topology {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) : (CategoryTheory.Limits.colimit F).str = ⨆ (j : J), TopologicalSpace.coinduced (⇑(CategoryTheory.Limits.colimit.ι F j)) (F.obj j).str

theorem TopCat.colimit_isOpen_iff {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) (U : Set ↑(CategoryTheory.Limits.colimit F)) : IsOpen U ↔ ∀ (j : J), IsOpen (⇑(CategoryTheory.Limits.colimit.ι F j) ⁻¹' U)

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)