Theorems · Theorem · category theory

CategoryTheory.BinaryCofan.isVanKampen_mk

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y)
  (cofans : (X Y : C) → CategoryTheory.Limits.BinaryCofan X Y)
  (colimits : (X Y : C) → CategoryTheory.Limits.IsColimit (cofans X Y))
  (cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PullbackCone f g)
  (limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.IsLimit (cones f g)),
  (∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
      CategoryTheory.CategoryStruct.comp αX c.inl = CategoryTheory.CategoryStruct.comp (cofans X' Y').inl f →
        CategoryTheory.CategoryStruct.comp αY c.inr = CategoryTheory.CategoryStruct.comp (cofans X' Y').inr f →
          CategoryTheory.IsPullback (cofans X' Y').inl αX f c.inl ∧
            CategoryTheory.IsPullback (cofans X' Y').inr αY f c.inr) →
    ∀
      (h₂ :
        {Z : C} →
          (f : Z ⟶ c.pt) →
            CategoryTheory.Limits.IsColimit
              (CategoryTheory.Limits.BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)),
      CategoryTheory.IsVanKampenColimit c

Defined in

Mathlib.CategoryTheory.Limits.VanKampen

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category