Sheaves for the coherent topology

This file characterises sheaves for the coherent topology

Main result

• isSheaf_coherent: a presheaf of types for the is a sheaf for the coherent topology if and only if it satisfies the sheaf condition with respect to every presieve consiting of a finite effective epimorphic family.

theorem CategoryTheory.isSheaf_coherent {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) P ↔ ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B), CategoryTheory.EffectiveEpiFamily X π → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π)

theorem CategoryTheory.coherentTopology.isSheaf_yoneda_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] (W : C) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) (CategoryTheory.yoneda.obj W)

Every Yoneda-presheaf is a sheaf for the coherent topology.

theorem CategoryTheory.coherentTopology.subcanonical {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Precoherent C] : CategoryTheory.Sheaf.Subcanonical (CategoryTheory.coherentTopology C)

The coherent topology on a precoherent category is subcanonical.