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))
- to_Top : Top
- 𝒪 : Top.presheaf C c.to_Top
A PresheafedSpace C is a topological space equipped with a presheaf of Cs.
@[instance]
Equations
@[simp]
theorem
algebraic_geometry.PresheafedSpace.as_coe
{C : Type u}
[𝒞 : category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.mk_coe
{C : Type u}
[𝒞 : category_theory.category C]
(to_Top : Top)
(𝒪 : Top.presheaf C to_Top) :
@[instance]
def
algebraic_geometry.PresheafedSpace.topological_space
{C : Type u}
[𝒞 : category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
Equations
- X.topological_space = X.to_Top.str
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) :
α.c ≫ category_theory.whisker_right (category_theory.nat_trans.op (topological_space.opens.map_iso α.base β.base w).inv) X.𝒪 = β.c → α = β
def
algebraic_geometry.PresheafedSpace.id
{C : Type u}
[𝒞 : category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
X.hom X
Equations
- X.id = {base := 𝟙 ↑X, c := (category_theory.functor.left_unitor X.𝒪).inv ≫ category_theory.whisker_right (category_theory.nat_trans.op (topological_space.opens.map_id X.to_Top).hom) X.𝒪}
def
algebraic_geometry.PresheafedSpace.comp
{C : Type u}
[𝒞 : category_theory.category C]
(X Y Z : algebraic_geometry.PresheafedSpace C) :
@[instance]
def
algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces
(C : Type u)
[𝒞 : category_theory.category 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
@[simp]
theorem
algebraic_geometry.PresheafedSpace.id_base
{C : Type u}
[𝒞 : category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
theorem
algebraic_geometry.PresheafedSpace.id_c
{C : Type u}
[𝒞 : category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
@[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.to_Top))ᵒᵖ) :
(𝟙 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) :
@[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.to_Top))ᵒᵖ) :
The forgetful functor from PresheafedSpace to Top.
Equations
- algebraic_geometry.PresheafedSpace.forget = {obj := λ (X : algebraic_geometry.PresheafedSpace C), ↑X, map := λ (X Y : algebraic_geometry.PresheafedSpace C) (f : X ⟶ Y), f.base, map_id' := _, map_comp' := _}
def
category_theory.functor.map_presheaf
{C : Type u}
[𝒞 : category_theory.category C]
{D : Type u}
[category_theory.category 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
@[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_𝒪
{C : Type u}
[𝒞 : category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
(X : algebraic_geometry.PresheafedSpace C) :
@[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)
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.𝒪 α ≫ (X.𝒪 ⋙ G).left_unitor.inv ≫ category_theory.whisker_right (category_theory.nat_trans.op (topological_space.opens.map_id X.to_Top).hom) (X.𝒪 ⋙ G)}, naturality' := _}