Theorems · Definition · category theory

TopCat.pullbackIsoProdSubtype

{X Y Z : TopCat} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      CategoryTheory.Limits.pullback f g ≅
        TopCat.of { p // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }

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

Defined in

Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Cited by

19 results in Mathlib

Foundations

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