mathlib documentation


Another version of the sheaf condition.

Given a family of open sets U : ι → opens X we can form the subcategory { V : opens X // ∃ i, V ≤ U i }, which has supr U as a cocone.

The sheaf condition on a presheaf F is equivalent to F sending the opposite of this cocone to a limit cone in C, for every U.

This condition is particularly nice when checking the sheaf condition because we don't need to do any case bashing (depending on whether we're looking at single or double intersections, or equivalently whether we're looking at the first or second object in an equalizer diagram).


def Top.presheaf.sheaf_condition.opens_le_cover {X : Top} {ι : Type v} (U : ι → topological_space.opens X) :
Type v

The category of open sets contained in some element of the cover.


An arbitrarily chosen index such that V ≤ U i.


supr U as a cocone over the opens sets contained in some element of the cover.

(In fact this is a colimit cocone.)

def Top.presheaf.sheaf_condition_opens_le_cover {C : Type u} [category_theory.category C] {X : Top} (F : Top.presheaf C X) :
Type (max u (v+1))

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

A presheaf is a sheaf if F sends the cone (opens_le_cover_cocone U).op to a limit cone. (Recall opens_le_cover_cocone U, has cone point supr U, mapping down to any V which is contained in some U i.)


The diagram consisting of the U i and U i ⊓ U j is cofinal in the diagram of all opens contained in some U i.

The sheaf condition in terms of a limit diagram over all { V : opens X // ∃ i, V ≤ U i } is equivalent to the reformulation in terms of a limit diagram over U i and U i ⊓ U j.