Theorems · Definition · category theory

CategoryTheory.Limits.PullbackCone.mk

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          {W : C} →
            (fst : W ⟶ X) →
              (snd : W ⟶ Y) →
                autoParam (CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g)
                    CategoryTheory.Limits.PullbackCone.mk._auto_1 →
                  CategoryTheory.Limits.PullbackCone f g

A pullback cone on f and g is determined by morphisms fst : W ⟶ X and snd : W ⟶ Y such that fst ≫ f = snd ≫ g.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Cited by

203 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category