Pullbacks and pushouts in the category of topological spaces #

source

@[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 := ⋯ }

Instances For

source

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

source

@[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 := ⋯ }

Instances For

source

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

source

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) ⋯

Instances For

source

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.

Instances For

source

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)

Instances For

source

@[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

source

@[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

source

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

source

@[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

source

@[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

source

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

source

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

source

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

source

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), ⋯⟩

source

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

source

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}

source

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

Equations

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

Instances For

source

theorem TopCat.isInducing_pullback_to_prod {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

IsInducing ⇑(CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))

source

@[deprecated TopCat.isInducing_pullback_to_prod]

theorem TopCat.inducing_pullback_to_prod {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

IsInducing ⇑(CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))

Alias of TopCat.isInducing_pullback_to_prod.

source

theorem TopCat.isEmbedding_pullback_to_prod {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

IsEmbedding ⇑(CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))

source

@[deprecated TopCat.isEmbedding_pullback_to_prod]

theorem TopCat.embedding_pullback_to_prod {X : TopCat} {Y : TopCat} {Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) :

IsEmbedding ⇑(CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))

Alias of TopCat.isEmbedding_pullback_to_prod.

source

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.

source

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}

source

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}

source

theorem TopCat.pullback_map_isEmbedding {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₁ : IsEmbedding ⇑i₁) (H₂ : 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₂) :

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

source

@[deprecated TopCat.pullback_map_isEmbedding]

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₁ : IsEmbedding ⇑i₁) (H₂ : 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₂) :

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

source

theorem TopCat.pullback_map_isOpenEmbedding {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₁ : IsOpenEmbedding ⇑i₁) (H₂ : 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₂) :

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

source

@[deprecated TopCat.pullback_map_isOpenEmbedding]

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₁ : IsOpenEmbedding ⇑i₁) (H₂ : 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₂) :

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

source

theorem TopCat.snd_isEmbedding_of_left {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} (H : IsEmbedding ⇑f) (g : Y ⟶ S) :

IsEmbedding ⇑(CategoryTheory.Limits.pullback.snd f g)

source

@[deprecated TopCat.snd_isEmbedding_of_left]

theorem TopCat.snd_embedding_of_left_embedding {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} (H : IsEmbedding ⇑f) (g : Y ⟶ S) :

IsEmbedding ⇑(CategoryTheory.Limits.pullback.snd f g)

Alias of TopCat.snd_isEmbedding_of_left.

source

theorem TopCat.fst_isEmbedding_of_right {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : IsEmbedding ⇑g) :

IsEmbedding ⇑(CategoryTheory.Limits.pullback.fst f g)

source

@[deprecated TopCat.fst_isEmbedding_of_right]

theorem TopCat.fst_embedding_of_right_embedding {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : IsEmbedding ⇑g) :

IsEmbedding ⇑(CategoryTheory.Limits.pullback.fst f g)

Alias of TopCat.fst_isEmbedding_of_right.

source

theorem TopCat.isEmbedding_of_pullback {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : IsEmbedding ⇑f) (H₂ : IsEmbedding ⇑g) :

IsEmbedding ⇑(CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)

source

@[deprecated TopCat.isEmbedding_of_pullback]

theorem TopCat.embedding_of_pullback_embeddings {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : IsEmbedding ⇑f) (H₂ : IsEmbedding ⇑g) :

IsEmbedding ⇑(CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)

Alias of TopCat.isEmbedding_of_pullback.

source

theorem TopCat.snd_isOpenEmbedding_of_left {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} (H : IsOpenEmbedding ⇑f) (g : Y ⟶ S) :

IsOpenEmbedding ⇑(CategoryTheory.Limits.pullback.snd f g)

source

@[deprecated TopCat.snd_isOpenEmbedding_of_left]

theorem TopCat.snd_openEmbedding_of_left_openEmbedding {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} (H : IsOpenEmbedding ⇑f) (g : Y ⟶ S) :

IsOpenEmbedding ⇑(CategoryTheory.Limits.pullback.snd f g)

Alias of TopCat.snd_isOpenEmbedding_of_left.

source

theorem TopCat.fst_isOpenEmbedding_of_right {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : IsOpenEmbedding ⇑g) :

IsOpenEmbedding ⇑(CategoryTheory.Limits.pullback.fst f g)

source

@[deprecated TopCat.fst_isOpenEmbedding_of_right]

theorem TopCat.fst_openEmbedding_of_right_openEmbedding {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (H : IsOpenEmbedding ⇑g) :

IsOpenEmbedding ⇑(CategoryTheory.Limits.pullback.fst f g)

Alias of TopCat.fst_isOpenEmbedding_of_right.

source

theorem TopCat.isOpenEmbedding_of_pullback_open_embeddings {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : IsOpenEmbedding ⇑f) (H₂ : IsOpenEmbedding ⇑g) :

IsOpenEmbedding ⇑(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.

source

@[deprecated TopCat.isOpenEmbedding_of_pullback_open_embeddings]

theorem TopCat.openEmbedding_of_pullback_open_embeddings {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} {g : Y ⟶ S} (H₁ : IsOpenEmbedding ⇑f) (H₂ : IsOpenEmbedding ⇑g) :

IsOpenEmbedding ⇑(CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)

Alias of TopCat.isOpenEmbedding_of_pullback_open_embeddings.

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

source

theorem TopCat.fst_iso_of_right_embedding_range_subset {X : TopCat} {Y : TopCat} {S : TopCat} (f : X ⟶ S) {g : Y ⟶ S} (hg : IsEmbedding ⇑g) (H : Set.range ⇑f ⊆ Set.range ⇑g) :

CategoryTheory.IsIso (CategoryTheory.Limits.pullback.fst f g)

source

theorem TopCat.snd_iso_of_left_embedding_range_subset {X : TopCat} {Y : TopCat} {S : TopCat} {f : X ⟶ S} (hf : IsEmbedding ⇑f) (g : Y ⟶ S) (H : Set.range ⇑g ⊆ Set.range ⇑f) :

CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)

source

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)

source

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)

source

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

source

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

source

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)

source

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)

Documentation

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Pullbacks and pushouts in the category of topological spaces #