Pullbacks and pushouts in the category of topological spaces #
theorem
TopCat.pullbackFst_apply
{X Y 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
theorem
TopCat.pullbackSnd_apply
{X Y 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
The explicit pullback cone of X, Y given by { p : X × Y // f p.1 = g p.2 }.
Equations
Instances For
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 Y 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)
Instances For
@[simp]
theorem
TopCat.pullbackIsoProdSubtype_inv_fst_apply
{X Y 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_apply
{X Y 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_apply
{X Y 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 Y 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 Y 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 : Topology.IsEmbedding g)
:
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
@[deprecated TopCat.isInducing_pullback_to_prod]
Alias of TopCat.isInducing_pullback_to_prod.
@[deprecated TopCat.isEmbedding_pullback_to_prod]
Alias of TopCat.isEmbedding_pullback_to_prod.
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.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 Y 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 Y 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_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 ⇑i₁)
(H₂ : Topology.IsEmbedding ⇑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.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
@[deprecated TopCat.pullback_map_isEmbedding]
theorem
TopCat.pullback_map_embedding_of_embeddings
{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 ⇑i₁)
(H₂ : Topology.IsEmbedding ⇑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.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
Alias of TopCat.pullback_map_isEmbedding.
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 ⇑i₁)
(H₂ : Topology.IsOpenEmbedding ⇑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.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
@[deprecated TopCat.pullback_map_isOpenEmbedding]
theorem
TopCat.pullback_map_openEmbedding_of_open_embeddings
{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 ⇑i₁)
(H₂ : Topology.IsOpenEmbedding ⇑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.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
Alias of TopCat.pullback_map_isOpenEmbedding.
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 ⇑f)
(g : Y ⟶ S)
:
@[deprecated TopCat.snd_isEmbedding_of_left]
theorem
TopCat.snd_embedding_of_left_embedding
{X Y S : TopCat}
{f : X ⟶ S}
(H : Topology.IsEmbedding ⇑f)
(g : Y ⟶ S)
:
Alias of TopCat.snd_isEmbedding_of_left.
theorem
TopCat.fst_isEmbedding_of_right
{X Y S : TopCat}
(f : X ⟶ S)
{g : Y ⟶ S}
(H : Topology.IsEmbedding ⇑g)
:
@[deprecated TopCat.fst_isEmbedding_of_right]
theorem
TopCat.fst_embedding_of_right_embedding
{X Y S : TopCat}
(f : X ⟶ S)
{g : Y ⟶ S}
(H : Topology.IsEmbedding ⇑g)
:
Alias of TopCat.fst_isEmbedding_of_right.
theorem
TopCat.isEmbedding_of_pullback
{X Y S : TopCat}
{f : X ⟶ S}
{g : Y ⟶ S}
(H₁ : Topology.IsEmbedding ⇑f)
(H₂ : Topology.IsEmbedding ⇑g)
:
@[deprecated TopCat.isEmbedding_of_pullback]
theorem
TopCat.embedding_of_pullback_embeddings
{X Y S : TopCat}
{f : X ⟶ S}
{g : Y ⟶ S}
(H₁ : Topology.IsEmbedding ⇑f)
(H₂ : Topology.IsEmbedding ⇑g)
:
Alias of TopCat.isEmbedding_of_pullback.
theorem
TopCat.snd_isOpenEmbedding_of_left
{X Y S : TopCat}
{f : X ⟶ S}
(H : Topology.IsOpenEmbedding ⇑f)
(g : Y ⟶ S)
:
@[deprecated TopCat.snd_isOpenEmbedding_of_left]
theorem
TopCat.snd_openEmbedding_of_left_openEmbedding
{X Y S : TopCat}
{f : X ⟶ S}
(H : Topology.IsOpenEmbedding ⇑f)
(g : Y ⟶ S)
:
Alias of TopCat.snd_isOpenEmbedding_of_left.
theorem
TopCat.fst_isOpenEmbedding_of_right
{X Y S : TopCat}
(f : X ⟶ S)
{g : Y ⟶ S}
(H : Topology.IsOpenEmbedding ⇑g)
:
@[deprecated TopCat.fst_isOpenEmbedding_of_right]
theorem
TopCat.fst_openEmbedding_of_right_openEmbedding
{X Y S : TopCat}
(f : X ⟶ S)
{g : Y ⟶ S}
(H : Topology.IsOpenEmbedding ⇑g)
:
Alias of TopCat.fst_isOpenEmbedding_of_right.
theorem
TopCat.isOpenEmbedding_of_pullback
{X Y S : TopCat}
{f : X ⟶ S}
{g : Y ⟶ S}
(H₁ : Topology.IsOpenEmbedding ⇑f)
(H₂ : Topology.IsOpenEmbedding ⇑g)
:
If X ⟶ S, Y ⟶ S are open embeddings, then so is X ×ₛ Y ⟶ S.
@[deprecated TopCat.isOpenEmbedding_of_pullback]
theorem
TopCat.isOpenEmbedding_of_pullback_open_embeddings
{X Y S : TopCat}
{f : X ⟶ S}
{g : Y ⟶ S}
(H₁ : Topology.IsOpenEmbedding ⇑f)
(H₂ : Topology.IsOpenEmbedding ⇑g)
:
Alias of TopCat.isOpenEmbedding_of_pullback.
If X ⟶ S, Y ⟶ S are open embeddings, then so is X ×ₛ Y ⟶ S.
@[deprecated TopCat.isOpenEmbedding_of_pullback]
theorem
TopCat.openEmbedding_of_pullback_open_embeddings
{X Y S : TopCat}
{f : X ⟶ S}
{g : Y ⟶ S}
(H₁ : Topology.IsOpenEmbedding ⇑f)
(H₂ : Topology.IsOpenEmbedding ⇑g)
:
Alias of TopCat.isOpenEmbedding_of_pullback.
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 ⇑g)
(H : Set.range ⇑f ⊆ Set.range ⇑g)
:
theorem
TopCat.snd_iso_of_left_embedding_range_subset
{X Y S : TopCat}
{f : X ⟶ S}
(hf : Topology.IsEmbedding ⇑f)
(g : Y ⟶ S)
(H : Set.range ⇑g ⊆ Set.range ⇑f)
:
theorem
TopCat.pullback_snd_image_fst_preimage
{X Y 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 Y 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)