Theorems · Theorem · category theory

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},
  Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom i₁) →
    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 ``

Defined in

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Cited by

3 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound