Sheaves for the coherent topology

This file characterises sheaves for the coherent topology

Main result

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

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

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

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

instance CategoryTheory.coherentTopology.subcanonical (C : Type u_1) [Category.{v_1, u_1} C] [Precoherent C] : (coherentTopology C).Subcanonical

The coherent topology on a precoherent category is subcanonical.