Theorems · Definition · category theory

CategoryTheory.Presieve.IsSheaf

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

A presheaf is a sheaf for a topology if it is a sheaf for every sieve in the topology. If the given topology is given by a pretopology, isSheaf_pretopology shows it suffices to check the sheaf condition at presieves in the pretopology.

Defined in

Mathlib.CategoryTheory.Sites.SheafOfTypes

Cited by

66 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category