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.