Theorems · Definition · category theory

CategoryTheory.Limits.pullback.lift

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasPullback f g] →
            (h : W ⟶ X) →
              (k : W ⟶ Y) →
                autoParam (CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
                    CategoryTheory.Limits.pullback.lift._auto_1 →
                  (W ⟶ CategoryTheory.Limits.pullback f g)

A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism pullback.lift : W ⟶ pullback f g.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Cited by

114 results in Mathlib

Foundations

Depth 24 from the axioms, rests on 157 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullback