mathlib documentation

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.

source
@[instance]
def Top.presheaf.sheaf_condition.subsingleton {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] {X : Top} (F : Top.presheaf C X) :
subsingleton F.sheaf_condition

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

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
source
def Top.presheaf.sheaf_condition_punit {X : Top} (F : Top.presheaf (category_theory.discrete punit) X) :
F.sheaf_condition

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

Equations
source
@[instance]
def Top.presheaf.sheaf_condition_inhabited {X : Top} (F : Top.presheaf (category_theory.discrete punit) X) :
inhabited F.sheaf_condition

Equations
source
def Top.presheaf.sheaf_condition_equiv_of_iso {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] {X : Top} {F G : Top.presheaf C X} (α : F ≅ G) :
F.sheaf_condition ≃ G.sheaf_condition

Transfer the sheaf condition across an isomorphism of presheaves.

Equations
source
structure Top.sheaf (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] (X : Top) :
Type (max u (v+1))

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

source
@[instance]
def Top.category_theory.category (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] (X : Top) :
category_theory.category (Top.sheaf C X)

Equations
source
@[instance]
def Top.sheaf_inhabited (X : Top) :
inhabited (Top.sheaf (category_theory.discrete punit) X)

Equations
source
@[instance]
def Top.sheaf.forget.faithful (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] (X : Top) :
category_theory.faithful (Top.sheaf.forget C X)

source
def Top.sheaf.forget (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] (X : Top) :
Top.sheaf C X ⥤ Top.presheaf C X

The forgetful functor from sheaves to presheaves.

Equations
source
@[instance]
def Top.sheaf.forget.full (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] (X : Top) :
category_theory.full (Top.sheaf.forget C X)