Local properties of sheaves #
In this file we study properties of sheaves that can be checked on a covering family of objects.
Main results #
CategoryTheory.Sheaf.isIso_iff_of_coversTop: A morphism of sheaves is an isomorphism if it is one on a cover.
theorem CategoryTheory.Sheaf.isIso_of_coversTop {C : Type u_1} [Category.{v_1, u_1} C] {K : GrothendieckTopology C} {A : Type u_2} [Category.{v_2, u_2} A] {ι : Type u_3} {X : ι → C} (hX : K.CoversTop X) {F G : Sheaf K A} {f : F ⟶ G} (h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)) :
IsIso f
A sheaf morphism is an isomorphism if it becomes one after pulling back along each element of a covering family.
theorem CategoryTheory.Sheaf.isIso_iff_of_coversTop {C : Type u_1} [Category.{v_1, u_1} C] {K : GrothendieckTopology C} {A : Type u_2} [Category.{v_2, u_2} A] {ι : Type u_3} {X : ι → C} (hX : K.CoversTop X) {F G : Sheaf K A} (f : F ⟶ G) :
A sheaf morphism is an isomorphism iff it becomes one after pulling back along each element of a covering family.