Stalks #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For a presheaf F on a topological space X, valued in some category C, the stalk of F at the point x : X is defined as the colimit of the composition of the inclusion of categories (nhds x)ᵒᵖ ⥤ (opens X)ᵒᵖ and the functor F : (opens X)ᵒᵖ ⥤ C. For an open neighborhood U of x, we define the map F.germ x : F.obj (op U) ⟶ F.stalk x as the canonical morphism into this colimit.

Taking stalks is functorial: For every point x : X we define a functor stalk_functor C x, sending presheaves on X to objects of C. Furthermore, for a map f : X ⟶ Y between topological spaces, we define stalk_pushforward as the induced map on the stalks (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x.

Some lemmas about stalks and germs only hold for certain classes of concrete categories. A basic property of forgetful functors of categories of algebraic structures (like Mon, CommRing,...) is that they preserve filtered colimits. Since stalks are filtered colimits, this ensures that the stalks of presheaves valued in these categories behave exactly as for Type-valued presheaves. For example, in germ_exist we prove that in such a category, every element of the stalk is the germ of a section.

Furthermore, if we require the forgetful functor to reflect isomorphisms and preserve limits (as is the case for most algebraic structures), we have access to the unique gluing API and can prove further properties. Most notably, in is_iso_iff_stalk_functor_map_iso, we prove that in such a category, a morphism of sheaves is an isomorphism if and only if all of its stalk maps are isomorphisms.

See also the definition of "algebraic structures" in the stacks project: https://stacks.math.columbia.edu/tag/007L