Documentation

Mathlib.CategoryTheory.Sites.Equivalence

Equivalences of sheaf categories #

Given a site (C, J) and a category D which is equivalent to C, with C and D possibly large and possibly in different universes, we transport the Grothendieck topology J on C to D and prove that the sheaf categories are equivalent.

We also prove that sheafification and the property HasSheafCompose transport nicely over this equivalence, and apply it to essentially small sites. We also provide instances for existence of sufficiently small limits in the sheaf category on the essentially small site.

Main definitions #

The functor in the equivalence of sheaf categories.

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

    The inverse in the equivalence of sheaf categories.

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

      The unit iso in the equivalence of sheaf categories.

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

        The counit iso in the equivalence of sheaf categories.

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

          The equivalence of sheaf categories.

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

            An auxiliary definition for the sheafification adjunction.

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

              Transporting and sheafifying is left adjoint to taking the underlying presheaf.

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

                Transport HasSheafify along an equivalence of sites.

                Transporting to a small model and sheafifying there is left adjoint to the underlying presheaf functor

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