Theorems · Theorem · category theory

CategoryTheory.isPullback_of_cofan_isVanKampen

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C] {ι : Type u_3}
  {X : ι → C} {c : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsVanKampenColimit c →
    ∀ (i j : ι) [inst_2 : DecidableEq ι],
      CategoryTheory.IsPullback
        (if h : j = i then CategoryTheory.eqToHom ⋯
        else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X i)))
        (if h : j = i then CategoryTheory.eqToHom ⋯
        else CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.initial.to (X j)))
        (c.inj i) (c.inj j)

Defined in

Mathlib.CategoryTheory.Limits.VanKampen

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasInitialDecidableEq