Theorems · Theorem · category theory

CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C] {X : C}
  (S : CategoryTheory.Sieve X),
  S ∈ (CategoryTheory.extensiveTopology C) X ↔
    ∃ α,
      ∃ (_ : Finite α),
        ∃ Y π,
          Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

Defined in

Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.FinitaryPreExtensive