mathlib documentation

topology.sheaves.sheaf_condition.pairwise_intersections

Equivalent formulations of the sheaf condition #

We give an equivalent formulation of the sheaf condition.

Given any indexed type ι, we define overlap ι, a category with objects corresponding to

Any open cover U : ι → opens X provides a functor diagram U : overlap ι ⥤ (opens X)ᵒᵖ.

There is a canonical cone over this functor, cone U, whose cone point is supr U, and in fact this is a limit cone.

A presheaf F : presheaf C X is a sheaf precisely if it preserves this limit. We express this in two equivalent ways, as

An alternative formulation of the sheaf condition (which we prove equivalent to the usual one below as is_sheaf_iff_is_sheaf_pairwise_intersections).

A presheaf is a sheaf if F sends the cone (pairwise.cocone U).op to a limit cone. (Recall pairwise.cocone U has cone point supr U, mapping down to the U i and the U i ⊓ U j.)

Equations

An alternative formulation of the sheaf condition (which we prove equivalent to the usual one below as is_sheaf_iff_is_sheaf_preserves_limit_pairwise_intersections).

A presheaf is a sheaf if F preserves the limit of pairwise.diagram U. (Recall pairwise.diagram U is the diagram consisting of the pairwise intersections U i ⊓ U j mapping into the open sets U i. This diagram has limit supr U.)

Equations

The remainder of this file shows that these conditions are equivalent to the usual sheaf condition.

The sheaf condition in terms of an equalizer diagram is equivalent to the reformulation in terms of a limit diagram over U i and U i ⊓ U j.

The sheaf condition in terms of an equalizer diagram is equivalent to the reformulation in terms of the presheaf preserving the limit of the diagram consisting of the U i and U i ⊓ U j.

For a sheaf F, F(U ∪ V) is the pullback of F(U) ⟶ F(U ∩ V) and F(V) ⟶ F(U ∩ V). This is the pullback cone.

Equations

(Implementation). Every cone over F(U) ⟶ F(U ∩ V) and F(V) ⟶ F(U ∩ V) factors through F(U ∪ V). TODO: generalize to C without products.

Equations

For a sheaf F, F(U ∪ V) is the pullback of F(U) ⟶ F(U ∩ V) and F(V) ⟶ F(U ∩ V).

Equations