Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {S : C}
  {ι : Type u_2} [Small.{max w v, u_2} ι] {X : ι → C} (f : (i : ι) → X i ⟶ S)
  {c : CategoryTheory.Limits.Cofan fun i => CategoryTheory.uliftYoneda.{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.uliftYoneda.{w, v, u}.map (f i))

Defined in

Mathlib.CategoryTheory.Sites.LocallySurjective

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySmall