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 consisting of a finite effective epimorphic family.
theorem
CategoryTheory.isSheaf_coherent
{C : Type u_1}
[Category.{u_2, u_1} C]
[Precoherent C]
(P : Functor Cᵒᵖ (Type w))
:
Presieve.IsSheaf (coherentTopology C) P ↔ ∀ (B : C) (α : Type) [inst : 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.{u_2, 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.{u_2, u_1} C]
[Precoherent C]
:
(coherentTopology C).Subcanonical
The coherent topology on a precoherent category is subcanonical.