Theorems · Theorem · category theory

CategoryTheory.GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_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} [inst_2 : Small.{w, u_2} ι] {X : ι → C}
  (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Sieve.ofArrows X f ∈ J S ↔
    CategoryTheory.Presheaf.IsLocallySurjective J
      (CategoryTheory.Limits.Sigma.desc fun i => CategoryTheory.shrinkYoneda.{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.CategoryCategoryTheory.LocallySmallSmall