Pullbacks and pushouts in the category of topological spaces #
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
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
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
@[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) }
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
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}
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₃ : 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₂)
:
If the map S ⟶ T
is mono, then there is a description of the image of W ×ₛ X ⟶ Y ×ₜ Z
.
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_openEmbedding_of_left_openEmbedding
{X : TopCat}
{Y : TopCat}
{S : TopCat}
{f : X ⟶ S}
(H : OpenEmbedding ↑f)
(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 ↑g)
:
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₁ : OpenEmbedding ↑f)
(H₂ : OpenEmbedding ↑g)
:
If X ⟶ S
, Y ⟶ S
are open embeddings, then so is X ×ₛ Y ⟶ S
.
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
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
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)