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))

carrier : Top
presheaf : Top.presheaf C c.carrier

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

@[instance]

def algebraic_geometry.PresheafedSpace.coe_carrier {C : Type u} [category_theory.category C] :

has_coe (algebraic_geometry.PresheafedSpace C) Top

Equations

algebraic_geometry.PresheafedSpace.coe_carrier = {coe := λ (X : algebraic_geometry.PresheafedSpace C), X.carrier}

@[simp]

theorem algebraic_geometry.PresheafedSpace.as_coe {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

X.carrier = ↑X

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

@[instance]

def algebraic_geometry.PresheafedSpace.topological_space {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

topological_space ↥X

Equations

X.topological_space = X.carrier.str

def algebraic_geometry.PresheafedSpace.const {C : Type u} [category_theory.category C] (X : Top) (Z : C) :

algebraic_geometry.PresheafedSpace C

The constant presheaf on X with value Z.

Equations

algebraic_geometry.PresheafedSpace.const X Z = {carrier := X, presheaf := {obj := λ (U : (topological_space.opens ↥X)ᵒᵖ), Z, map := λ (U V : (topological_space.opens ↥X)ᵒᵖ) (f : U ⟶ V), 𝟙 Z, map_id' := _, map_comp' := _}}

@[instance]

def algebraic_geometry.PresheafedSpace.inhabited {C : Type u} [category_theory.category C] [inhabited C] :

inhabited (algebraic_geometry.PresheafedSpace C)

Equations

algebraic_geometry.PresheafedSpace.inhabited = {default := algebraic_geometry.PresheafedSpace.const (Top.of pempty) (default C)}

structure algebraic_geometry.PresheafedSpace.hom {C : Type u} [category_theory.category C] (X Y : algebraic_geometry.PresheafedSpace C) :

Type v

base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ c.base _* X.presheaf

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} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} (α β : X.hom Y) (w : α.base = β.base) (h : α.c ≫ category_theory.whisker_right (category_theory.nat_trans.op (topological_space.opens.map_iso α.base β.base w).inv) X.presheaf = β.c) :

α = β

def algebraic_geometry.PresheafedSpace.id {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

X.hom X

The identity morphism of a PresheafedSpace.

Equations

X.id = {base := 𝟙 ↑X, c := (category_theory.functor.left_unitor X.presheaf).inv ≫ category_theory.whisker_right (category_theory.nat_trans.op (topological_space.opens.map_id X.carrier).hom) X.presheaf}

@[instance]

def algebraic_geometry.PresheafedSpace.hom_inhabited {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

inhabited (X.hom X)

Equations

X.hom_inhabited = {default := X.id}

def algebraic_geometry.PresheafedSpace.comp {C : Type u} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (α : X.hom Y) (β : Y.hom Z) :

X.hom Z

Composition of morphisms of PresheafedSpaces.

Equations

algebraic_geometry.PresheafedSpace.comp α β = {base := α.base ≫ β.base, c := β.c ≫ category_theory.whisker_left (topological_space.opens.map β.base).op α.c ≫ (Top.presheaf.pushforward.comp X.presheaf α.base β.base).inv}

@[instance]

def algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces (C : Type u) [category_theory.category C] :

category_theory.category (algebraic_geometry.PresheafedSpace C)

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

algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces C = {to_category_struct := {to_has_hom := {hom := algebraic_geometry.PresheafedSpace.hom _inst_1}, id := algebraic_geometry.PresheafedSpace.id _inst_1, comp := λ (X Y Z : algebraic_geometry.PresheafedSpace C) (f : X ⟶ Y) (g : Y ⟶ Z), algebraic_geometry.PresheafedSpace.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

theorem algebraic_geometry.PresheafedSpace.id_base {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

(𝟙 X).base = 𝟙 ↑X

theorem algebraic_geometry.PresheafedSpace.id_c {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

(𝟙 X).c = (category_theory.functor.left_unitor X.presheaf).inv ≫ category_theory.whisker_right (category_theory.nat_trans.op (topological_space.opens.map_id X.carrier).hom) X.presheaf

@[simp]

theorem algebraic_geometry.PresheafedSpace.id_c_app {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) (U : (topological_space.opens ↥(X.carrier))ᵒᵖ) :

(𝟙 X).c.app U = category_theory.eq_to_hom _

@[simp]

theorem algebraic_geometry.PresheafedSpace.comp_base {C : Type u} [category_theory.category C] {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} [category_theory.category C] {X Y Z : algebraic_geometry.PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (U : (topological_space.opens ↥(Z.carrier))ᵒᵖ) :

(α ≫ β).c.app U = β.c.app U ≫ α.c.app (opposite.op ((topological_space.opens.map β.base).obj (opposite.unop U))) ≫ (Top.presheaf.pushforward.comp X.presheaf α.base β.base).inv.app U

theorem algebraic_geometry.PresheafedSpace.congr_app {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U : (topological_space.opens ↥(Y.carrier))ᵒᵖ) :

α.c.app U = β.c.app U ≫ X.presheaf.map (category_theory.eq_to_hom _)

@[simp]

theorem algebraic_geometry.PresheafedSpace.forget_obj (C : Type u) [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

(algebraic_geometry.PresheafedSpace.forget C).obj X = ↑X

def algebraic_geometry.PresheafedSpace.forget (C : Type u) [category_theory.category C] :

algebraic_geometry.PresheafedSpace C ⥤ Top

The forgetful functor from PresheafedSpace to Top.

Equations

algebraic_geometry.PresheafedSpace.forget C = {obj := λ (X : algebraic_geometry.PresheafedSpace C), ↑X, map := λ (X Y : algebraic_geometry.PresheafedSpace C) (f : X ⟶ Y), f.base, map_id' := _, map_comp' := _}

@[simp]

theorem algebraic_geometry.PresheafedSpace.forget_map (C : Type u) [category_theory.category C] (X Y : algebraic_geometry.PresheafedSpace C) (f : X ⟶ Y) :

(algebraic_geometry.PresheafedSpace.forget C).map f = f.base

def algebraic_geometry.PresheafedSpace.restrict {C : Type u} [category_theory.category C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) (f : U ⟶ ↑X) (h : open_embedding ⇑f) :

algebraic_geometry.PresheafedSpace C

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

Equations

X.restrict f h = {carrier := U, presheaf := _.functor.op ⋙ X.presheaf}

@[simp]

theorem algebraic_geometry.PresheafedSpace.restrict_carrier {C : Type u} [category_theory.category C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) (f : U ⟶ ↑X) (h : open_embedding ⇑f) :

(X.restrict f h).carrier = U

@[simp]

theorem algebraic_geometry.PresheafedSpace.restrict_presheaf {C : Type u} [category_theory.category C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) (f : U ⟶ ↑X) (h : open_embedding ⇑f) :

(X.restrict f h).presheaf = _.functor.op ⋙ X.presheaf

def algebraic_geometry.PresheafedSpace.of_restrict {C : Type u} [category_theory.category C] (U : Top) (X : algebraic_geometry.PresheafedSpace C) (f : U ⟶ ↑X) (h : open_embedding ⇑f) :

X.restrict f h ⟶ X

The map from the restriction of a presheafed space.

Equations

algebraic_geometry.PresheafedSpace.of_restrict U X f h = {base := f, c := {app := λ (V : (topological_space.opens ↥(X.carrier))ᵒᵖ), X.presheaf.map (⇑((_.adjunction.hom_equiv ((topological_space.opens.map f).obj (opposite.unop V)) (opposite.unop V)).symm) (𝟙 ((topological_space.opens.map f).obj (opposite.unop V)))).op, naturality' := _}}

@[simp]

theorem algebraic_geometry.PresheafedSpace.of_restrict_c_app {C : Type u} [category_theory.category C] (U : Top) (X : algebraic_geometry.PresheafedSpace C) (f : U ⟶ ↑X) (h : open_embedding ⇑f) (V : (topological_space.opens ↥(X.carrier))ᵒᵖ) :

(algebraic_geometry.PresheafedSpace.of_restrict U X f h).c.app V = X.presheaf.map (⇑((_.adjunction.hom_equiv ((topological_space.opens.map f).obj (opposite.unop V)) (opposite.unop V)).symm) (𝟙 ((topological_space.opens.map f).obj (opposite.unop V)))).op

@[simp]

theorem algebraic_geometry.PresheafedSpace.of_restrict_base {C : Type u} [category_theory.category C] (U : Top) (X : algebraic_geometry.PresheafedSpace C) (f : U ⟶ ↑X) (h : open_embedding ⇑f) :

(algebraic_geometry.PresheafedSpace.of_restrict U X f h).base = f

def algebraic_geometry.PresheafedSpace.to_restrict_top {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

X ⟶ X.restrict ⊤.inclusion _

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

Equations

X.to_restrict_top = {base := {to_fun := λ (x : ↥↑X), ⟨x, trivial⟩, continuous_to_fun := _}, c := {app := λ (U : (topological_space.opens ↥((X.restrict ⊤.inclusion _).carrier))ᵒᵖ), X.presheaf.map (category_theory.hom_of_le _).op, naturality' := _}}

@[simp]

theorem algebraic_geometry.PresheafedSpace.to_restrict_top_c_app {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) (U : (topological_space.opens ↥((X.restrict ⊤.inclusion _).carrier))ᵒᵖ) :

X.to_restrict_top.c.app U = X.presheaf.map (category_theory.hom_of_le _).op

@[simp]

theorem algebraic_geometry.PresheafedSpace.to_restrict_top_base_to_fun_val {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) (x : ↥↑X) :

(⇑(X.to_restrict_top.base) x).val = x

def algebraic_geometry.PresheafedSpace.restrict_top_iso {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

X.restrict ⊤.inclusion _ ≅ X

The isomorphism from the restriction to the top subspace.

Equations

X.restrict_top_iso = {hom := algebraic_geometry.PresheafedSpace.of_restrict ((topological_space.opens.to_Top ↑X).obj ⊤) X ⊤.inclusion _, inv := X.to_restrict_top, hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem algebraic_geometry.PresheafedSpace.restrict_top_iso_hom {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

X.restrict_top_iso.hom = algebraic_geometry.PresheafedSpace.of_restrict ((topological_space.opens.to_Top ↑X).obj ⊤) X ⊤.inclusion _

@[simp]

theorem algebraic_geometry.PresheafedSpace.restrict_top_iso_inv {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

X.restrict_top_iso.inv = X.to_restrict_top

@[simp]

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

algebraic_geometry.PresheafedSpace.Γ.obj X = (opposite.unop X).presheaf.obj (opposite.op ⊤)

@[simp]

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

algebraic_geometry.PresheafedSpace.Γ.map f = f.unop.c.app (opposite.op ⊤) ≫ (opposite.unop Y).presheaf.map (topological_space.opens.le_map_top f.unop.base ⊤).op

def algebraic_geometry.PresheafedSpace.Γ {C : Type u} [category_theory.category C] :

(algebraic_geometry.PresheafedSpace C)ᵒᵖ ⥤ C

The global sections, notated Gamma.

Equations

algebraic_geometry.PresheafedSpace.Γ = {obj := λ (X : (algebraic_geometry.PresheafedSpace C)ᵒᵖ), (opposite.unop X).presheaf.obj (opposite.op ⊤), map := λ (X Y : (algebraic_geometry.PresheafedSpace C)ᵒᵖ) (f : X ⟶ Y), f.unop.c.app (opposite.op ⊤) ≫ (opposite.unop Y).presheaf.map (topological_space.opens.le_map_top f.unop.base ⊤).op, map_id' := _, map_comp' := _}

theorem algebraic_geometry.PresheafedSpace.Γ_obj_op {C : Type u} [category_theory.category C] (X : algebraic_geometry.PresheafedSpace C) :

algebraic_geometry.PresheafedSpace.Γ.obj (opposite.op X) = X.presheaf.obj (opposite.op ⊤)

theorem algebraic_geometry.PresheafedSpace.Γ_map_op {C : Type u} [category_theory.category C] {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) :

algebraic_geometry.PresheafedSpace.Γ.map f.op = f.c.app (opposite.op ⊤) ≫ X.presheaf.map (topological_space.opens.le_map_top f.base ⊤).op

def category_theory.functor.map_presheaf {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] (F : C ⥤ D) :

algebraic_geometry.PresheafedSpace C ⥤ algebraic_geometry.PresheafedSpace 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

F.map_presheaf = {obj := λ (X : algebraic_geometry.PresheafedSpace C), {carrier := X.carrier, presheaf := X.presheaf ⋙ F}, map := λ (X Y : algebraic_geometry.PresheafedSpace C) (f : X ⟶ Y), {base := f.base, c := category_theory.whisker_right f.c F}, map_id' := _, map_comp' := _}

@[simp]

theorem category_theory.functor.map_presheaf_obj_X {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] (F : C ⥤ D) (X : algebraic_geometry.PresheafedSpace C) :

↑(F.map_presheaf.obj X) = ↑X

@[simp]

theorem category_theory.functor.map_presheaf_obj_presheaf {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] (F : C ⥤ D) (X : algebraic_geometry.PresheafedSpace C) :

(F.map_presheaf.obj X).presheaf = X.presheaf ⋙ F

@[simp]

theorem category_theory.functor.map_presheaf_map_f {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] (F : C ⥤ D) {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) :

(F.map_presheaf.map f).base = f.base

@[simp]

theorem category_theory.functor.map_presheaf_map_c {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] (F : C ⥤ D) {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) :

(F.map_presheaf.map f).c = category_theory.whisker_right f.c F

def category_theory.nat_trans.on_presheaf {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] {F G : C ⥤ D} (α : F ⟶ G) :

G.map_presheaf ⟶ F.map_presheaf

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

Equations

category_theory.nat_trans.on_presheaf α = {app := λ (X : algebraic_geometry.PresheafedSpace C), {base := 𝟙 ↑(G.map_presheaf.obj X), c := category_theory.whisker_left X.presheaf α ≫ (X.presheaf ⋙ G).left_unitor.inv ≫ category_theory.whisker_right (category_theory.nat_trans.op (topological_space.opens.map_id X.carrier).hom) (X.presheaf ⋙ G)}, naturality' := _}