mathlib3 documentation

topology.sheaves.sheafify

Sheafification of Type valued presheaves #

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

We construct the sheafification of a Type valued presheaf, as the subsheaf of dependent functions into the stalks consisting of functions which are locally germs.

We show that the stalks of the sheafification are isomorphic to the original stalks, via stalk_to_fiber which evaluates a germ of a dependent function at a point.

We construct a morphism to_sheafify from a presheaf to (the underlying presheaf of) its sheafification, given by sending a section to its collection of germs.

Future work #

Show that the map induced on stalks by to_sheafify is the inverse of stalk_to_fiber.

Show sheafification is a functor from presheaves to sheaves, and that it is the left adjoint of the forgetful functor, following https://stacks.math.columbia.edu/tag/007X.

The prelocal predicate on functions into the stalks, asserting that the function is equal to a germ.

Equations

The local predicate on functions into the stalks, asserting that the function is locally equal to a germ.

Equations
def Top.presheaf.sheafify {X : Top} (F : Top.presheaf (Type v) X) :

The sheafification of a Type valued presheaf, defined as the functions into the stalks which are locally equal to germs.

Equations
noncomputable def Top.presheaf.to_sheafify {X : Top} (F : Top.presheaf (Type v) X) :

The morphism from a presheaf to its sheafification, sending each section to its germs. (This forms the unit of the adjunction.)

Equations
noncomputable def Top.presheaf.stalk_to_fiber {X : Top} (F : Top.presheaf (Type v) X) (x : X) :

The natural morphism from the stalk of the sheafification to the original stalk. In sheafify_stalk_iso we show this is an isomorphism.

Equations
noncomputable def Top.presheaf.sheafify_stalk_iso {X : Top} (F : Top.presheaf (Type v) X) (x : X) :

The isomorphism betweeen a stalk of the sheafification and the original stalk.

Equations