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]
def
algebraic_geometry.PresheafedSpace.coe_to_Top
{C : Type u}
[๐ : category_theory.category C] :
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
structure
algebraic_geometry.PresheafedSpace.hom
{C : Type u}
[๐ : category_theory.category C] :
algebraic_geometry.PresheafedSpace C โ algebraic_geometry.PresheafedSpace C โ Type v
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
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
- algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces C = {to_category_struct := {to_has_hom := {hom := algebraic_geometry.PresheafedSpace.hom ๐}, id := algebraic_geometry.PresheafedSpace.id ๐, comp := algebraic_geometry.PresheafedSpace.comp ๐}, id_comp' := _, comp_id' := _, assoc' := _}
@[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' := _}