Theorems · Theorem · category theory

CategoryTheory.BinaryCofan.isVanKampen_iff

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y),
  CategoryTheory.IsVanKampenColimit c ↔
    ∀ {X' Y' : C} (c' : CategoryTheory.Limits.BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      CategoryTheory.CategoryStruct.comp αX c.inl = CategoryTheory.CategoryStruct.comp c'.inl f →
        CategoryTheory.CategoryStruct.comp αY c.inr = CategoryTheory.CategoryStruct.comp c'.inr f →
          (Nonempty (CategoryTheory.Limits.IsColimit c') ↔
            CategoryTheory.IsPullback c'.inl αX f c.inl ∧ CategoryTheory.IsPullback c'.inr αY f c.inr)

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.Category