mathlib documentation

algebraic_geometry.presheafed_space

Presheafed spaces #

Introduces the category of topological spaces equipped with a presheaf (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.PresheafedSpace (C : Type u) [category_theory.category C] :
Type (max u (v+1))

A PresheafedSpace C is a topological space equipped with a presheaf of Cs.

@[simp]
theorem algebraic_geometry.PresheafedSpace.mk_coe {C : Type u} [category_theory.category C] (carrier : Top) (presheaf : Top.presheaf C carrier) :
{carrier := carrier, presheaf := presheaf} = carrier

The constant presheaf on X with value Z.

Equations

A morphism between presheafed spaces X and Y consists of a continuous map f between the underlying topological spaces, and a (notice contravariant!) map from the presheaf on Y to the pushforward of the presheaf on X via f.

@[instance]

The category of PresheafedSpaces. Morphisms are pairs, a continuous map and a presheaf map from the presheaf on the target to the pushforward of the presheaf on the source.

Equations
@[simp]

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

Equations

The map to the restriction of a presheafed space along the canonical inclusion from the top subspace.

Equations

The isomorphism from the restriction to the top subspace.

Equations

We can apply a functor F : C ⥤ D to the values of the presheaf in any PresheafedSpace C, giving a functor PresheafedSpace C ⥤ PresheafedSpace D

Equations