# mathlibdocumentation

topology.sheaves.sheaf

# Sheaves #

We define sheaves on a topological space, with values in an arbitrary category with products.

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

We provide the instance category (sheaf C X) as the full subcategory of presheaves, and the fully faithful functor sheaf.forget : sheaf C X ⥤ presheaf C X.

## Equivalent conditions #

While the "official" definition is in terms of an equalizer diagram, in src/topology/sheaves/sheaf_condition/pairwise_intersections.lean and in src/topology/sheaves/sheaf_condition/open_le_cover.lean we provide two equivalent conditions (and prove they are equivalent).

The first is that F.obj U is the limit point of the diagram consisting of all the F.obj (U i) and F.obj (U i ⊓ U j). (That is, we explode the equalizer of two products out into its component pieces.)

The second is that F.obj U is the limit point of the diagram constisting of all the F.obj V, for those V : opens X such that V ≤ U i for some i. (This condition is particularly easy to state, and perhaps should become the "official" definition.)

def Top.presheaf.is_sheaf {C : Type u} {X : Top} (F : X) :
Prop

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
• F.is_sheaf = ∀ ⦃ι : Type v⦄ (U : ι → ,

The presheaf valued in punit over any topological space is a sheaf.

theorem Top.presheaf.is_sheaf_of_iso {C : Type u} {X : Top} {F G : X} (α : F G) (h : F.is_sheaf) :

Transfer the sheaf condition across an isomorphism of presheaves.

theorem Top.presheaf.is_sheaf_iso_iff {C : Type u} {X : Top} {F G : X} (α : F G) :
@[protected, instance]
def Top.sheaf.category (C : Type u) (X : Top) :
def Top.sheaf (C : Type u) (X : Top) :
Type (max u v)

A sheaf C X is a presheaf of objects from C over a (bundled) topological space X, satisfying the sheaf condition.

Equations
@[protected, instance]
def Top.sheaf_inhabited (X : Top) :
Equations
@[protected, instance]
def Top.sheaf.forget.faithful (C : Type u) (X : Top) :
def Top.sheaf.forget (C : Type u) (X : Top) :
X X

The forgetful functor from sheaves to presheaves.

Equations
@[protected, instance]
def Top.sheaf.forget.full (C : Type u) (X : Top) :
@[simp]
theorem Top.sheaf.id_app (C : Type u) (X : Top) (F : X) (t : ᵒᵖ) :
(𝟙 F).app t = 𝟙 (F.val.obj t)
@[simp]
theorem Top.sheaf.comp_app (C : Type u) (X : Top) {F G H : X} (f : F G) (g : G H) (t : ᵒᵖ) :
(f g).app t = f.app t g.app t