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

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

An alternative formulation of the sheaf condition (which we prove equivalent to the usual one below as sheaf_condition_equiv_sheaf_condition_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
@[nolint]

An alternative formulation of the sheaf condition (which we prove equivalent to the usual one below as sheaf_condition_equiv_sheaf_condition_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.