Documentation

Mathlib.CategoryTheory.Sites.Sheafification

Sheafification #

Given a site (C, J) we define a typeclass HasSheafify J A saying that the inclusion functor from A-valued sheaves on C to presheaves admits a left exact left adjoint (sheafification).

Note: to access the HasSheafify instance for suitable concrete categories, import the file Mathlib.CategoryTheory.Sites.LeftExact.

@[reducible, inline]

A proposition saying that the inclusion functor from sheaves to presheaves admits a left adjoint.

Equations
Instances For

    HasSheafify means that the inclusion functor from sheaves to presheaves admits a left exact left adjiont (sheafification).

    Given a finite limit preserving functor F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A and an adjunction adj : F ⊣ sheafToPresheaf J A, use HasSheafify.mk' to construct a HasSheafify instance.

    Instances
      @[reducible, inline]

      The sheafification of a presheaf P.

      Equations
      Instances For
        @[reducible, inline]

        The canonical map from P to its sheafification.

        Equations
        Instances For
          @[reducible, inline]

          The canonical map on sheafifications induced by a morphism.

          Equations
          Instances For

            Given a sheaf Q and a morphism P ⟶ Q, construct a morphism from sheafify J P to Q.

            Equations
            Instances For

              A sheaf P is isomorphic to its own sheafification.

              Equations
              Instances For