Sheafification of Type-valued presheaves

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 stalkToFiber which evaluates a germ of a dependent function at a point.

We construct a morphism toSheafify 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 toSheafify is the inverse of stalkToFiber.

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.

def TopCat.Presheaf.Sheafify.isGerm {X : TopCat} (F : Presheaf (Type v) X) : PrelocalPredicate fun (x : ↑X) => F.stalk x

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

def TopCat.Presheaf.Sheafify.isLocallyGerm {X : TopCat} (F : Presheaf (Type v) X) : LocalPredicate fun (x : ↑X) => F.stalk x

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

def TopCat.Presheaf.sheafify {X : TopCat} (F : Presheaf (Type v) X) : Sheaf (Type v) X

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

noncomputable def TopCat.Presheaf.toSheafify {X : TopCat} (F : Presheaf (Type v) X) : F ⟶ F.sheafify.obj

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

noncomputable def TopCat.Presheaf.stalkToFiber {X : TopCat} (F : Presheaf (Type v) X) (x : ↑X) : F.sheafify.presheaf.stalk x ⟶ F.stalk x

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

theorem TopCat.Presheaf.stalkToFiber_surjective {X : TopCat} (F : Presheaf (Type v) X) (x : ↑X) : Function.Surjective (F.stalkToFiber x)

theorem TopCat.Presheaf.stalkToFiber_injective {X : TopCat} (F : Presheaf (Type v) X) (x : ↑X) : Function.Injective (F.stalkToFiber x)

noncomputable def TopCat.Presheaf.sheafifyStalkIso {X : TopCat} (F : Presheaf (Type v) X) (x : ↑X) : F.sheafify.presheaf.stalk x ≅ F.stalk x

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

theorem TopCat.Presheaf.stalkFunctor_map_unit_toSheafify_isIso {X : TopCat} (p₀ : ↑X) (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] [CategoryTheory.Limits.HasTerminal C] (𝓕 : Presheaf C X) [CategoryTheory.HasWeakSheafify (Opens.grothendieckTopology ↑X) C] : CategoryTheory.IsIso ((stalkFunctor C p₀).map (CategoryTheory.toSheafify (Opens.grothendieckTopology ↑X) 𝓕))

Given a presheaf 𝓕, the induced map on stalks of CategoryTheory.toSheafify, 𝓕ₓ ⟶ 𝓕⁺ₓ, is an isomorphism