# mathlib3documentation

algebraic_geometry.presheafed_space

# Presheafed 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 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 (w+1))

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

Instances for algebraic_geometry.PresheafedSpace
@[protected, instance]
Equations
@[simp]
theorem algebraic_geometry.PresheafedSpace.mk_coe {C : Type u} (carrier : Top) (presheaf : carrier) :
{carrier := carrier, presheaf := presheaf} = carrier
@[protected, instance]
Equations
def algebraic_geometry.PresheafedSpace.const {C : Type u} (X : Top) (Z : C) :

The constant presheaf on X with value Z.

Equations
@[protected, instance]
Equations
structure algebraic_geometry.PresheafedSpace.hom {C : Type u}  :
Type (max v w)

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.

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

The identity morphism of a PresheafedSpace.

Equations
@[protected, instance]
Equations
def algebraic_geometry.PresheafedSpace.comp {C : Type u} {X Y Z : algebraic_geometry.PresheafedSpace C} (α : X.hom Y) (β : Y.hom Z) :
X.hom Z

Composition of morphisms of PresheafedSpaces.

Equations
theorem algebraic_geometry.PresheafedSpace.comp_c {C : Type u} {X Y Z : algebraic_geometry.PresheafedSpace C} (α : X.hom Y) (β : Y.hom Z) :
= β.c .map α.c
@[protected, 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.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
@[protected, instance]
Equations
@[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)))

Sometimes rewriting with comp_c_app doesn't work because of dependent type issues. In that case, erw comp_c_app_assoc might make progress. The lemma comp_c_app_assoc is also better suited for rewrites in the opposite direction.

theorem algebraic_geometry.PresheafedSpace.comp_c_app_assoc {C : Type u} {X Y Z : algebraic_geometry.PresheafedSpace C} (α : X Y) (β : Y Z) (U : ᵒᵖ) {X' : C} (f' : ((α β).base _* X.presheaf).obj U X') :
β).c.app U f' = β.c.app U α.c.app (opposite.op (opposite.unop U))) f'
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
Instances for algebraic_geometry.PresheafedSpace.forget
@[simp]
@[simp]

An isomorphism of PresheafedSpaces is a homeomorphism of the underlying space, and a natural transformation between the sheaves.

Equations

Isomorphic PresheafedSpaces have natural isomorphic presheaves.

Equations
@[simp]
@[protected, instance]
@[protected, instance]

This could be used in conjunction with category_theory.nat_iso.is_iso_of_is_iso_app.

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

Equations
@[simp]

The map from the restriction of a presheafed space.

Equations
Instances for algebraic_geometry.PresheafedSpace.of_restrict
@[simp]
@[protected, instance]

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

Equations
@[simp]
@[simp]

The isomorphism from the restriction to the top subspace.

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

The global sections, notated Gamma.

Equations
def category_theory.functor.map_presheaf {C : Type u} {D : Type u} (F : C D) :

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