mathlib documentation

algebraic_geometry.sheafed_space

Sheafed spaces #

Introduces the category of topological spaces equipped with a sheaf (taking values in an arbitrary target category C.)

We further describe how to apply functors and natural transformations to the values of the presheaves.

A SheafedSpace C is a topological space equipped with a sheaf of Cs.

@[simp]
theorem algebraic_geometry.SheafedSpace.mk_coe {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] (carrier : Top) (presheaf : Top.presheaf C carrier) (h : {carrier := carrier, presheaf := presheaf}.presheaf.sheaf_condition) :
{to_PresheafedSpace := {carrier := carrier, presheaf := presheaf}, sheaf_condition := h} = carrier