mathlib3 documentation


Sheafed spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

structure algebraic_geometry.SheafedSpace (C : Type u) [category_theory.category C] :
Type (max u (v+1))

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

Instances for algebraic_geometry.SheafedSpace

Extract the sheaf C (X : Top) from a SheafedSpace C.

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

The restriction of a sheafed space along an open embedding into the space.