Theorems · Theorem · category theory

CategoryTheory.Presieve.isSheaf_coverage

∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] (K : CategoryTheory.Coverage C)
  (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
  CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ↔
    ∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R

The main theorem of this file: Given a coverage K on C, a Type*-valued presheaf on C is a sheaf for K if and only if it is a sheaf for the associated Grothendieck topology.

Defined in

Mathlib.CategoryTheory.Sites.Coverage

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category