Theorems · Definition · category theory

isBinaryProductOfIsTerminalIsPullback

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) →
      (c : CategoryTheory.Limits.Cone F) →
        {X : C} →
          (hX : CategoryTheory.Limits.IsTerminal X) →
            (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ X) →
              (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ X) →
                CategoryTheory.Limits.IsLimit
                    (CategoryTheory.Limits.PullbackCone.mk (c.π.app { as := CategoryTheory.Limits.WalkingPair.left })
                      (c.π.app { as := CategoryTheory.Limits.WalkingPair.right }) ⋯) →
                  CategoryTheory.Limits.IsLimit c

If a span is the pullback span over the terminal object, then it is a binary product.

Defined in

Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category