Pullbacks and pushouts in the category of topological spaces

@[reducible, inline]

abbrev TopCat.pullbackFst {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : of { p : ↑X × ↑Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 } ⟶ X

The first projection from the pullback.

theorem TopCat.pullbackFst_apply {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (x : ↑(of { p : ↑X × ↑Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 })) : (CategoryTheory.ConcreteCategory.hom (pullbackFst f g)) x = (↑x).1

@[reducible, inline]

abbrev TopCat.pullbackSnd {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : of { p : ↑X × ↑Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 } ⟶ Y

The second projection from the pullback.

theorem TopCat.pullbackSnd_apply {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (x : ↑(of { p : ↑X × ↑Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 })) : (CategoryTheory.ConcreteCategory.hom (pullbackSnd f g)) x = (↑x).2

def TopCat.pullbackCone {X Y 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 }.

def TopCat.pullbackConeIsLimit {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.IsLimit (pullbackCone f g)

The constructed cone is a limit.

def TopCat.pullbackIsoProdSubtype {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.pullback f g ≅ of { p : ↑X × ↑Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }

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

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_fst {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).inv (CategoryTheory.Limits.pullback.fst f g) = pullbackFst f g

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_fst_assoc {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : TopCat} (h : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp (pullbackFst f g) h

theorem TopCat.pullbackIsoProdSubtype_inv_fst_apply {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (x : { p : ↑X × ↑Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) ((CategoryTheory.ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) x) = (↑x).1

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_snd {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).inv (CategoryTheory.Limits.pullback.snd f g) = pullbackSnd f g

@[simp]

theorem TopCat.pullbackIsoProdSubtype_inv_snd_assoc {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : TopCat} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp (pullbackSnd f g) h

theorem TopCat.pullbackIsoProdSubtype_inv_snd_apply {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (x : { p : ↑X × ↑Y // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) ((CategoryTheory.ConcreteCategory.hom (pullbackIsoProdSubtype f g).inv) x) = (↑x).2

theorem TopCat.pullbackIsoProdSubtype_hom_fst {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).hom (pullbackFst f g) = CategoryTheory.Limits.pullback.fst f g

theorem TopCat.pullbackIsoProdSubtype_hom_snd {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackIsoProdSubtype f g).hom (pullbackSnd f g) = CategoryTheory.Limits.pullback.snd f g

theorem TopCat.pullbackIsoProdSubtype_hom_apply {X Y Z : TopCat} {f : X ⟶ Z} {g : Y ⟶ Z} (x : ↑(CategoryTheory.Limits.pullback f g)) : (CategoryTheory.ConcreteCategory.hom (pullbackIsoProdSubtype f g).hom) x = ⟨((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) x, (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) x), ⋯⟩

theorem TopCat.pullback_topology {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.pullback f g).str = TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))) X.str ⊓ TopologicalSpace.induced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))) Y.str

theorem TopCat.range_pullback_to_prod {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))) = {x : ↑(X ⨯ Y) | (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f)) x = (CategoryTheory.ConcreteCategory.hom (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 : Topology.IsEmbedding g) : { p : X × Y // f p.1 = g p.2 } ≃ₜ ↑(f ⁻¹' Set.range g)

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

theorem TopCat.isInducing_pullback_to_prod {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g)))

theorem TopCat.isEmbedding_pullback_to_prod {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g)))

theorem TopCat.range_pullback_map {W X Y Z S 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.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) = ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom i₁) ∩ ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom 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 Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) = {x : ↑X | ∃ (y : ↑Y), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) y}

theorem TopCat.pullback_snd_range {X Y S : TopCat} (f : X ⟶ S) (g : Y ⟶ S) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) = {y : ↑Y | ∃ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) y}

theorem TopCat.pullback_map_isEmbedding {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₁)) (H₂ : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom 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₂) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (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_isOpenEmbedding {W X Y Z S T : TopCat} (f₁ : W ⟶ S) (f₂ : X ⟶ S) (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) {i₁ : W ⟶ Y} {i₂ : X ⟶ Z} (H₁ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₁)) (H₂ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom 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₂) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (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_isEmbedding_of_left {X Y S : TopCat} {f : X ⟶ S} (H : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (g : Y ⟶ S) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))

theorem TopCat.fst_isEmbedding_of_right {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))

theorem TopCat.isEmbedding_of_pullback {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (H₂ : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one))

theorem TopCat.snd_isOpenEmbedding_of_left {X Y S : TopCat} {f : X ⟶ S} (H : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (g : Y ⟶ S) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))

theorem TopCat.fst_isOpenEmbedding_of_right {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))

theorem TopCat.isOpenEmbedding_of_pullback {X Y S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (H₂ : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (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 Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (hg : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g)) (H : Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)) : CategoryTheory.IsIso (CategoryTheory.Limits.pullback.fst f g)

theorem TopCat.snd_iso_of_left_embedding_range_subset {X Y S : TopCat} {f : X ⟶ S} (hf : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (g : Y ⟶ S) (H : Set.range ⇑(CategoryTheory.ConcreteCategory.hom g) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f)) : CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)

theorem TopCat.pullback_snd_image_fst_preimage {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set ↑X) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) '' (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) ⁻¹' U) = ⇑(CategoryTheory.ConcreteCategory.hom g) ⁻¹' (⇑(CategoryTheory.ConcreteCategory.hom f) '' U)

theorem TopCat.pullback_fst_image_snd_preimage {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set ↑Y) : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) '' (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) ⁻¹' U) = ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' (⇑(CategoryTheory.ConcreteCategory.hom g) '' U)

theorem TopCat.isOpen_iff_of_isColimit_cofork {X Y : TopCat} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Cofork f g) (hc : CategoryTheory.Limits.IsColimit c) (U : Set ↑c.pt) : IsOpen U ↔ IsOpen (⇑(CategoryTheory.ConcreteCategory.hom c.π) ⁻¹' U)

theorem TopCat.isQuotientMap_of_isColimit_cofork {X Y : TopCat} {f g : X ⟶ Y} (c : CategoryTheory.Limits.Cofork f g) (hc : CategoryTheory.Limits.IsColimit c) : Topology.IsQuotientMap ⇑(CategoryTheory.ConcreteCategory.hom c.π)

theorem TopCat.coequalizer_isOpen_iff {X Y : TopCat} {f g : X ⟶ Y} (U : Set ↑(CategoryTheory.Limits.coequalizer f g)) : IsOpen U ↔ IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.coequalizer.π f g)) ⁻¹' U)