Theorems · Definition · category theory

CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : CategoryTheory.Limits.FormalCoproduct C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (pb :
              (i : Function.Pullback f.f g.f) →
                CategoryTheory.Limits.PullbackCone
                  (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯)) (g.φ (↑i).2)) →
            ((i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i)) →
              (T : CategoryTheory.Limits.FormalCoproduct C) →
                (T ⟶ (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt) ≃
                  { p // CategoryTheory.CategoryStruct.comp p.1 f = CategoryTheory.CategoryStruct.comp p.2 g }

The Equiv that witnesses that pullbackCone f g pb is actually a pullback. This is the universal property of pullbacks.

Defined in

Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category