Theorems · Theorem · category theory

CategoryTheory.Limits.CoproductDisjoint.of_cofan

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} {c : CategoryTheory.Limits.Cofan X}
  (hc : CategoryTheory.Limits.IsColimit c) [∀ (i : ι), CategoryTheory.Mono (c.inj i)]
  (s : {i j : ι} → i ≠ j → CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j))
  (hs : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsLimit (s hij))
  (H : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsInitial (s hij).pt),
  CategoryTheory.Limits.CoproductDisjoint X

Defined in

Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Mono