Theorems · Theorem · category theory

CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff

∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : CategoryTheory.Precoverage C}
  (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
  CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ {X Y : C} {f : Y ⟶ X},
      ∀ R ∈ J.coverings X,
        CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.generate R)).arrows

The main theorem of this file: given a precoverage J on C, a Type*-valued presheaf on C is a sheaf for the associated Grothendieck topology if and only if it is a sheaf for all pullback sieves of presieves in J.

Defined in

Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category