Documentation

Mathlib.CategoryTheory.Sites.ConstantSheaf

The constant sheaf #

We define the constant sheaf functor (the sheafification of the constant presheaf) constantSheaf : D ⥤ Sheaf J D and prove that it is left adjoint to evaluation at a terminal object (see constantSheafAdj).

We also define a predicate on sheaves, Sheaf.IsConstant, saying that a sheaf is in the essential image of the constant sheaf functor.

Main results #

The constant presheaf functor is left adjoint to evaluation at a terminal object.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The functor which maps an object of D to the constant sheaf at that object, i.e. the sheafification of the constant presheaf.

    Equations
    Instances For

      A sheaf is constant if it is in the essential image of the constant sheaf functor.

      Instances

        If the constant sheaf functor is fully faithful, then a sheaf is constant if and only if the counit of the constant sheaf adjunction applied to it is an isomorphism.

        The constant sheaf functor commutes up to isomorphism the equivalence of sheaf categories induced by a dense subsite.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The constant sheaf functor commutes up to isomorphism the inverse equivalence of sheaf categories induced by a dense subsite.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The constant sheaf functor commutes with sheafCompose J U up to isomorphism, provided that U preserves sheafification.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For