Theorems · Theorem · category theory

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.ConcreteCategory.hom (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) =
    ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst g₁ g₂)) ⁻¹'
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom i₁) ∩
      ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd g₁ g₂)) ⁻¹'
        Set.range ⇑(CategoryTheory.ConcreteCategory.hom i₂)

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

Defined in

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Mono