Documentation

Mathlib.CategoryTheory.Sites.Plus

The plus construction for presheaves. #

This file contains the construction of P⁺, for a presheaf P : Cᵒᵖ ⥤ D where C is endowed with a grothendieck topology J.

See https://stacks.math.columbia.edu/tag/00W1 for details.

The diagram whose colimit defines the values of plus.

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

    A helper definition used to define the morphisms for plus.

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

      A natural transformation P ⟶ Q induces a natural transformation between diagrams whose colimits define the values of plus.

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

        J.diagram P, as a functor in P.

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

          The plus construction, associating a presheaf to any presheaf. See plusFunctor below for a functorial version.

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

            An auxiliary definition used in plus below.

            Equations
            Instances For

              The plus construction, a functor sending P to J.plusObj P.

              Equations
              Instances For

                The canonical map from P to J.plusObj P. See toPlusNatTrans for a functorial version.

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

                  The natural transformation from the identity functor to plus.

                  Equations
                  Instances For
                    @[simp]

                    (P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺

                    The natural isomorphism between P and P⁺ when P is a sheaf.

                    Equations
                    Instances For

                      Lift a morphism P ⟶ Q to P⁺ ⟶ Q when Q is a sheaf.

                      Equations
                      Instances For