# mathlibdocumentation

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)  :
Type (max u (v+1))
• carrier : Top
• presheaf :

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

@[instance]

Equations
@[simp]

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

@[instance]

Equations

The constant presheaf on X with value Z.

Equations
@[instance]

Equations
structure algebraic_geometry.PresheafedSpace.hom {C : Type u}  :

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.

@[ext]
theorem algebraic_geometry.PresheafedSpace.ext {C : Type u} (α β : X.hom Y) (w : α.base = β.base) :
α = β

def algebraic_geometry.PresheafedSpace.id {C : Type u}  :
X.hom X

The identity morphism of a PresheafedSpace.

Equations
@[instance]

Equations
def algebraic_geometry.PresheafedSpace.comp {C : Type u} {X Y Z : algebraic_geometry.PresheafedSpace C} :
X.hom YY.hom ZX.hom Z

Composition of morphisms of PresheafedSpaces.

Equations
@[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]

@[simp]
theorem algebraic_geometry.PresheafedSpace.id_c_app {C : Type u} (U : ᵒᵖ) :
(𝟙 X).c.app U =

@[simp]
theorem algebraic_geometry.PresheafedSpace.comp_base {C : Type u} {X Y Z : algebraic_geometry.PresheafedSpace C} (f : X Y) (g : Y Z) :
(f g).base = f.base g.base

@[simp]
theorem algebraic_geometry.PresheafedSpace.comp_c_app {C : Type u} {X Y Z : algebraic_geometry.PresheafedSpace C} (α : X Y) (β : Y Z) (U : ᵒᵖ) :
β).c.app U = β.c.app U α.c.app (opposite.op (opposite.unop U))) .inv.app U

theorem algebraic_geometry.PresheafedSpace.congr_app {C : Type u} {α β : X Y} (h : α = β) (U : ᵒᵖ) :
α.c.app U = β.c.app U

@[simp]

The forgetful functor from PresheafedSpace to Top.

Equations
@[simp]
theorem algebraic_geometry.PresheafedSpace.forget_map (C : Type u) (f : X Y) :

def algebraic_geometry.PresheafedSpace.restrict {C : Type u} {U : Top} (f : U X) :

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

Equations
@[simp]
theorem algebraic_geometry.PresheafedSpace.restrict_carrier {C : Type u} {U : Top} (f : U X) (h : open_embedding f) :
(X.restrict f h).carrier = U

@[simp]

def algebraic_geometry.PresheafedSpace.of_restrict {C : Type u} (U : Top) (f : U X) (h : open_embedding f) :
X.restrict f h X

The map from the restriction of a presheafed space.

Equations
@[simp]
theorem algebraic_geometry.PresheafedSpace.of_restrict_base {C : Type u} (U : Top) (f : U X) (h : open_embedding f) :

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
@[simp]

@[simp]
theorem algebraic_geometry.PresheafedSpace.Γ_obj {C : Type u} (X : ᵒᵖ) :

@[simp]
theorem algebraic_geometry.PresheafedSpace.Γ_map {C : Type u} (X Y : ᵒᵖ) (f : X Y) :

The global sections, notated Gamma.

Equations
theorem algebraic_geometry.PresheafedSpace.Γ_map_op {C : Type u} (f : X Y) :

def category_theory.functor.map_presheaf {C : Type u} {D : Type u}  :

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
@[simp]
theorem category_theory.functor.map_presheaf_obj_X {C : Type u} {D : Type u} (F : C D)  :

@[simp]
theorem category_theory.functor.map_presheaf_obj_presheaf {C : Type u} {D : Type u} (F : C D)  :

@[simp]
theorem category_theory.functor.map_presheaf_map_f {C : Type u} {D : Type u} (F : C D) (f : X Y) :

@[simp]
theorem category_theory.functor.map_presheaf_map_c {C : Type u} {D : Type u} (F : C D) (f : X Y) :

def category_theory.nat_trans.on_presheaf {C : Type u} {D : Type u} {F G : C D} :
(F G)

A natural transformation induces a natural transformation between the map_presheaf functors.

Equations