Stalk-locality of free abelian representable sheaves

If U ⊆ V are opens and x ∈ U, the induced map from the free abelian sheaf represented by U to the one represented by V is an isomorphism on the stalk at x.

This is the local input for the injective-row half of the Cech-to-derived comparison. It lets us intersect a Cech cover with one chosen member without changing the resulting free representable resolution on stalks inside that member.

The proof is deliberately made before sheafification. The map is injective on every open. For surjectivity on the stalk, represent a germ over a neighborhood contained in U; on such a neighborhood the two representable hom-types are both singletons, so the induced map of free abelian groups is an isomorphism. The units of sheafification are isomorphisms on stalks, which then transports the result to sheaves.

noncomputable def CategoryTheory.Sheaf.freeAbelianYonedaPresheafMap {X : TopCat} {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) : (yoneda.obj U).comp AddCommGrpCat.free ⟶ (yoneda.obj V).comp AddCommGrpCat.free

The morphism of free abelian representable presheaves induced by an inclusion of opens.

Equations

• CategoryTheory.Sheaf.freeAbelianYonedaPresheafMap i = CategoryTheory.Functor.whiskerRight (CategoryTheory.yoneda.map i) AddCommGrpCat.free

noncomputable def CategoryTheory.Sheaf.freeAbelianYonedaSheafMap {X : TopCat} {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) : freeAbelianYonedaSheaf (Opens.grothendieckTopology ↑X) U ⟶ freeAbelianYonedaSheaf (Opens.grothendieckTopology ↑X) V

The morphism of free abelian representable sheaves induced by an inclusion of opens.

Equations

• CategoryTheory.Sheaf.freeAbelianYonedaSheafMap i = (CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat).map (CategoryTheory.Sheaf.freeAbelianYonedaPresheafMap i)

theorem CategoryTheory.Sheaf.freeAbelianYonedaSheafMap_stalk_isIso {X : TopCat} {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (x : ↑X) (hx : x ∈ U) : IsIso ((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).map (freeAbelianYonedaSheafMap i).hom)

A map of free abelian sheaves represented by U ⊆ V is an isomorphism on every stalk inside U.

theorem CategoryTheory.Sheaf.freeAbelianYonedaSheaf_stalk_isZero_of_not_mem {X : TopCat} (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∉ U) : Limits.IsZero ((TopCat.Presheaf.stalkFunctor AddCommGrpCat x).obj (freeAbelianYonedaSheaf (Opens.grothendieckTopology ↑X) U).obj)

The stalk at x of the free abelian sheaf represented by an open not containing x is zero.