Theorems · Definition · category theory

CompHausLike.pullback.lift

{P : TopCat → Prop} →
  {X Y B : CompHausLike P} →
    (f : X ⟶ B) →
      (g : Y ⟶ B) →
        [inst : CompHausLike.HasExplicitPullback f g] →
          {Z : CompHausLike P} →
            (a : Z ⟶ X) →
              (b : Z ⟶ Y) →
                CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g →
                  (Z ⟶ CompHausLike.pullback f g)

Construct a morphism to the explicit pullback given morphisms to the factors which are compatible with the maps to the base. This is essentially the universal property of the pullback.

Defined in

Mathlib.Topology.Category.CompHausLike.Limits

Cited by

6 results in Mathlib

Foundations

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

Assumes

CompHausLike.HasExplicitPullback