Isomorphisms of sheaves of modules are local #
A morphism of sheaves of modules is an isomorphism if it is one after restriction to every member of a cover of the terminal object. This lets one check an isomorphism involving a line bundle, such as its tensor evaluation map, on a cover of free rank-one trivializations.
This is the module-sheaf counterpart of Mathlib's local isomorphism criterion for sheaves.
theorem
SheafOfModules.isIso_of_coversTop
{C : Type u}
[CategoryTheory.Category.{w, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M N : SheafOfModules R}
{ι : Type x}
{X : ι → C}
(hX : J.CoversTop X)
(f : M ⟶ N)
(hf : ∀ (i : ι), CategoryTheory.IsIso (Hom.over f (X i)))
:
A morphism of sheaves of modules that is an isomorphism on every member of a covering family is an isomorphism globally.
theorem
SheafOfModules.isIso_iff_of_coversTop
{C : Type u}
[CategoryTheory.Category.{w, u} C]
{J : CategoryTheory.GrothendieckTopology C}
{R : CategoryTheory.Sheaf J RingCat}
{M N : SheafOfModules R}
{ι : Type x}
{X : ι → C}
(hX : J.CoversTop X)
(f : M ⟶ N)
:
A morphism of sheaves of modules is an isomorphism exactly when its restrictions to a cover are isomorphisms.