Theorems · Theorem · category theory

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

Defined in

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Mono