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}
[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]
:
The coherent topology on a precoherent category is subcanonical.