Theorems · Theorem · category theory

CategoryTheory.Presieve.isSheafFor_subsieve_aux

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w))
  {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X},
  S.arrows ≤ R →
    CategoryTheory.Presieve.IsSheafFor P S.arrows →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
          R f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f S).arrows) →
        CategoryTheory.Presieve.IsSheafFor P R

If a presieve R on X has a subsieve S such that: * P is a sheaf for S. * For every f in R, P is separated for the pullback of S along f, then P is a sheaf for R. This is closely related to [Elephant] C2.1.6(i).

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category