mathlib3 documentation

topology.sheaves.sheaf_condition.equalizer_products

The sheaf condition in terms of an equalizer of products #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Equations

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

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

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

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

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

The remainder of this file shows that the equalizer_products sheaf condition is equivalent to the pariwise_intersections sheaf condition.

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