Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {S : C} {ι : Type u_2} [Small.{w, u_2} ι] {X : ι → C}
  (f : (i : ι) → X i ⟶ S) {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.shrinkYoneda.{w, v, u}.obj (X i)}
  (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.Sieve.ofArrows X f ∈ J S ↔
    CategoryTheory.Presheaf.IsLocallySurjective J
      (CategoryTheory.Limits.Cofan.IsColimit.desc hc fun i => CategoryTheory.shrinkYoneda.{w, v, u}.map (f i))

Defined in

Mathlib.CategoryTheory.Sites.LocallySurjective

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.LocallySmallSmall