Theorems · Theorem · category theory

CategoryTheory.Limits.WidePullback.hom_ext

∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C}
  (g1 g2 : X ⟶ CategoryTheory.Limits.widePullback B objs arrows),
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.π arrows j) =
        CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.π arrows j)) →
    CategoryTheory.CategoryStruct.comp g1 (CategoryTheory.Limits.WidePullback.base arrows) =
        CategoryTheory.CategoryStruct.comp g2 (CategoryTheory.Limits.WidePullback.base arrows) →
      g1 = g2

Defined in

Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasWidePullback