mathlib documentation

topology.sheaves.sheaf_condition.equalizer_products

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).

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
@[simp]

Push forward a cover along an open embedding.

Equations

If F : presheaf C X is a presheaf, and oe : U ⟶ X is an open embedding, then the sheaf condition fork for a cover 𝒰 in U for the composition of oe and F is isomorphic to sheaf condition fork for oe '' 𝒰, precomposed with the isomorphism of indexing diagrams diagram.iso_of_open_embedding.

We use this to show that the restriction of sheaf along an open embedding is still a sheaf.

Equations