Documentation

Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

The sheaf condition in terms of an equalizer of products #

Here we set up the machinery for the "usual" definition of the sheaf condition, e.g. as in https://stacks.math.columbia.edu/tag/0072 in terms of an equalizer diagram where the two objects are ∏ᶜ F.obj (U i) and ∏ᶜ F.obj (U i) ⊓ (U j).

We show that this sheaf condition is equivalent to the "pairwise intersections" sheaf condition when the presheaf is valued in a category with products, and thereby equivalent to the default sheaf condition.

The product of the sections of a presheaf over a family of open sets.

Equations
Instances For

    The product of the sections of a presheaf over the pairwise intersections of a family of open sets.

    Equations
    Instances For

      The morphism Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j) whose components are given by the restriction maps from U i to U i ⊓ U j.

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

        The morphism Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j) whose components are given by the restriction maps from U j to U i ⊓ U j.

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

          The morphism F.obj U ⟶ Π F.obj (U i) whose components are given by the restriction maps from U j to U i ⊓ U j.

          Equations
          Instances For
            @[reducible, inline]

            The equalizer diagram for the sheaf condition.

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

              Isomorphic presheaves have isomorphic sheaf condition diagrams.

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

                If F G : presheaf C X are isomorphic presheaves, then the fork F U, the canonical cone of the sheaf condition diagram for F, is isomorphic to fork F G postcomposed with the corresponding isomorphism between sheaf condition diagrams.

                Equations
                Instances For

                  The sheaf condition for a F : presheaf C X requires that the morphism F.obj U ⟶ ∏ᶜ F.obj (U i) (where U is some open set which is the union of the U i) is the equalizer of the two morphisms ∏ᶜ F.obj (U i) ⟶ ∏ᶜ F.obj (U i) ⊓ (U j).

                  Equations
                  Instances For

                    The remainder of this file shows that the "equalizer products" sheaf condition is equivalent to the "pairwise intersections" sheaf condition.

                    Cones over diagram U ⋙ F are the same as a cones over the usual sheaf condition equalizer diagram.

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

                      The sheaf condition in terms of an equalizer diagram is equivalent to the default sheaf condition.