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
The equalizer diagram for the sheaf condition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The restriction map F.obj U ⟶ Π F.obj (U i)
gives a cone over the equalizer diagram
for the sheaf condition. The sheaf condition asserts this cone is a limit cone.
Equations
Instances For
Isomorphic presheaves have isomorphic piOpens
for any cover U
.
Equations
Instances For
Isomorphic presheaves have isomorphic piInters
for any cover U
.
Equations
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.
Implementation of SheafConditionPairwiseIntersections.coneEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of SheafConditionPairwiseIntersections.coneEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of SheafConditionPairwiseIntersections.coneEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of SheafConditionPairwiseIntersections.coneEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of SheafConditionPairwiseIntersections.coneEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of SheafConditionPairwiseIntersections.coneEquiv
.
Equations
Instances For
Implementation of SheafConditionPairwiseIntersections.coneEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
If SheafConditionEqualizerProducts.fork
is an equalizer,
then F.mapCone (cone U)
is a limit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If F.mapCone (cone U)
is a limit cone,
then SheafConditionEqualizerProducts.fork
is an equalizer.
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.