mathlib3 documentation

topology.category.Top.limits.pullbacks

Pullbacks in the category of topological spaces. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[reducible]
def Top.pullback_fst {X Y Z : Top} (f : X Z) (g : Y Z) :
Top.of {p // f p.fst = g p.snd} X

The first projection from the pullback.

@[reducible]
def Top.pullback_snd {X Y Z : Top} (f : X Z) (g : Y Z) :
Top.of {p // f p.fst = g p.snd} Y

The second projection from the pullback.

def Top.pullback_cone {X Y Z : Top} (f : X Z) (g : Y Z) :

The explicit pullback cone of X, Y given by { p : X × Y // f p.1 = g p.2 }.

Equations

The constructed cone is a limit.

Equations
noncomputable def Top.pullback_iso_prod_subtype {X Y Z : Top} (f : X Z) (g : Y Z) :

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

Equations
theorem Top.range_pullback_map {W X Y Z S T : Top} (f₁ : W S) (f₂ : X S) (g₁ : Y T) (g₂ : Z T) (i₁ : W Y) (i₂ : X Z) (i₃ : S T) [H₃ : category_theory.mono i₃] (eq₁ : f₁ i₃ = i₁ g₁) (eq₂ : f₂ i₃ = i₂ g₂) :

If the map S ⟶ T is mono, then there is a description of the image of W ×ₛ X ⟶ Y ×ₜ Z.

theorem Top.pullback_fst_range {X Y S : Top} (f : X S) (g : Y S) :
theorem Top.pullback_snd_range {X Y S : Top} (f : X S) (g : Y S) :
theorem Top.pullback_map_embedding_of_embeddings {W X Y Z S T : Top} (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₁ : f₁ i₃ = i₁ g₁) (eq₂ : f₂ i₃ = i₂ g₂) :
embedding (category_theory.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 Top.pullback_map_open_embedding_of_open_embeddings {W X Y Z S T : Top} (f₁ : W S) (f₂ : X S) (g₁ : Y T) (g₂ : Z T) {i₁ : W Y} {i₂ : X Z} (H₁ : open_embedding i₁) (H₂ : open_embedding i₂) (i₃ : S T) [H₃ : category_theory.mono i₃] (eq₁ : f₁ i₃ = i₁ g₁) (eq₂ : f₂ i₃ = i₂ g₂) :
open_embedding (category_theory.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

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