Documentation

Mathlib.CategoryTheory.Sites.Discrete

Discrete objects in sheaf categories. #

This file defines the notion of a discrete object in a sheaf category. A discrete sheaf in this context is a sheaf F such that the counit (F(*))^cst ⟶ F is an isomorphism. Here * denotes a particular chosen terminal object of the defining site, and cst denotes the constant sheaf.

It is convenient to take an arbitrary terminal object; one might want to use this construction to talk about discrete sheaves on a site which has a particularly convenient terminal object, such as the one element space in CompHaus.

Main results #

Future work #

@[reducible, inline]

A sheaf is discrete if it is a discrete object of the "underlying object" functor from the sheaf category to the target category.

Equations
Instances For

    The constant sheaf functor commutes up to isomorphism with any equivalence of sheaf categories.

    This is an auxiliary definition used to prove Sheaf.isDiscrete_iff_of_equivalence below, which says that the property of a sheaf of being a discrete object is invariant under equivalence of sheaf categories.

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

      The constant sheaf functor commutes up to isomorphism with any equivalence of sheaf categories.

      This is an auxiliary definition used to prove Sheaf.isDiscrete_iff_of_equivalence below, which says that the property of a sheaf of being a discrete object is invariant under equivalence of sheaf categories.

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

        The constant sheaf functor commutes with sheafCompose up to isomorphism.

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