Theorems · Definition · category theory

CategoryTheory.Limits.Cone.ofPullbackCone

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} →
      CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
          (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) →
        CategoryTheory.Limits.Cone F

This is a helper construction that can be useful when verifying that a category has all pullbacks. Given F : WalkingCospan ⥤ C, which is really the same as cospan (F.map inl) (F.map inr), and a pullback cone on F.map inl and F.map inr, we get a cone on F. If you're thinking about using this, have a look at hasPullbacks_of_hasLimit_cospan, which you may find to be an easier way of achieving your goal.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category