Theorems · Definition · category theory

CategoryTheory.Limits.BinaryFan.IsLimit.mk

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (s : CategoryTheory.Limits.BinaryFan X Y) →
        (lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)) →
          (∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.fst = f) →
            (∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift f g) s.snd = g) →
              (∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt),
                  CategoryTheory.CategoryStruct.comp m s.fst = f →
                    CategoryTheory.CategoryStruct.comp m s.snd = g → m = lift f g) →
                CategoryTheory.Limits.IsLimit s

A convenient way to show that a binary fan is a limit.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category