Theorems · Definition · category theory

CategoryTheory.Presieve.IsSheafFor

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Functor Cᵒᵖ (Type w) → CategoryTheory.Presieve X → Prop

We define P to be a sheaf for the presieve R if every compatible family has a unique amalgamation. This is the definition of a sheaf for the given presieve given in C2.1.2 of [Elephant], and https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents. Using compatible_iff_sieveCompatible, this is equivalent to the definition of a sheaf in [MM92], Chapter III, Section 4.

Defined in

Mathlib.CategoryTheory.Sites.IsSheafFor

Cited by

111 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 91 definitions · uses propext, Quot.sound

Assumes

CategoryTheory.Category