Stalkwise isomorphisms are inverted by sheafification

TopCat.Presheaf.W_of_isIso_stalkFunctor_map: a morphism of presheaves of abelian groups on a topological space whose stalk maps are all isomorphisms lies in (Opens.grothendieckTopology X).W, the class sheafification inverts.

This is one direction of the stalkwise characterisation of J.W on a space. It matters because J.W unfolds to IsLocallyInjective and IsLocallySurjective, and Mathlib has no stalkwise criterion for the injective half — so a proof that goes through the halves separately cannot use stalks, while this lemma can.

The proof is the naturality square of toSheafify read on stalks: three of its four edges are isomorphisms, so the fourth is one too.

theorem TopCat.Presheaf.W_of_isIso_stalkFunctor_map {X : TopCat} {F G : Presheaf AddCommGrpCat X} (f : F ⟶ G) [∀ (x : ↑X), CategoryTheory.IsIso ((stalkFunctor AddCommGrpCat x).map f)] : (Opens.grothendieckTopology ↑X).W f

A stalkwise isomorphism of presheaves of abelian groups on a space is inverted by sheafification. One half of the stalkwise characterisation of J.W; the half needed to conclude local bijectivity from a stalk computation, without ever mentioning IsLocallyInjective — for which no stalkwise criterion exists in Mathlib.

The proof is the naturality square of toSheafify read on stalks: three of its four edges are isomorphisms, so the fourth is one too.