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)
[category_theory.category C] :
Type (max u v (w+1))
- carrier : Top
- presheaf : Top.presheaf C self.carrier
A PresheafedSpace C is a topological space equipped with a presheaf of Cs.
Instances for algebraic_geometry.PresheafedSpace
- algebraic_geometry.PresheafedSpace.has_sizeof_inst
- algebraic_geometry.PresheafedSpace.coe_carrier
- algebraic_geometry.PresheafedSpace.inhabited
- algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces
- algebraic_geometry.PresheafedSpace.category_theory.limits.has_colimits_of_shape
- algebraic_geometry.PresheafedSpace.category_theory.limits.has_colimits
@[protected, 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]
(carrier : Top)
(presheaf : Top.presheaf C carrier) :
@[protected, instance]
def
algebraic_geometry.PresheafedSpace.topological_space
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
Equations
- X.topological_space = X.carrier.str
def
algebraic_geometry.PresheafedSpace.const
{C : Type u}
[category_theory.category C]
(X : Top)
(Z : C) :
The constant presheaf on X with value Z.
@[protected, instance]
def
algebraic_geometry.PresheafedSpace.inhabited
{C : Type u}
[category_theory.category C]
[inhabited C] :
structure
algebraic_geometry.PresheafedSpace.hom
{C : Type u}
[category_theory.category C]
(X Y : algebraic_geometry.PresheafedSpace C) :
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
- algebraic_geometry.PresheafedSpace.hom.has_sizeof_inst
- algebraic_geometry.PresheafedSpace.hom_inhabited
@[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.eq_to_hom _) X.presheaf = β.c) :
α = β
theorem
algebraic_geometry.PresheafedSpace.hext
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(α β : X.hom Y)
(w : α.base = β.base)
(h : α.c == β.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.
@[protected, instance]
def
algebraic_geometry.PresheafedSpace.hom_inhabited
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
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.
theorem
algebraic_geometry.PresheafedSpace.comp_c
{C : Type u}
[category_theory.category C]
{X Y Z : algebraic_geometry.PresheafedSpace C}
(α : X.hom Y)
(β : Y.hom Z) :
(algebraic_geometry.PresheafedSpace.comp α β).c = β.c ≫ (Top.presheaf.pushforward C β.base).map α.c
@[protected, 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_quiver := {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) :
theorem
algebraic_geometry.PresheafedSpace.id_c
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
(𝟙 X).c = category_theory.eq_to_hom _
@[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))ᵒᵖ) :
@[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) :
@[protected, instance]
def
algebraic_geometry.PresheafedSpace.quiver.hom.has_coe_to_fun
{C : Type u}
[category_theory.category C]
(X Y : algebraic_geometry.PresheafedSpace C) :
theorem
algebraic_geometry.PresheafedSpace.coe_to_fun_eq
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(f : X ⟶ Y) :
@[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)))
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}
[category_theory.category C]
{X Y Z : algebraic_geometry.PresheafedSpace C}
(α : X ⟶ Y)
(β : Y ⟶ Z)
(U : (topological_space.opens ↥(Z.carrier))ᵒᵖ)
{X' : C}
(f' : ((α ≫ β).base _* X.presheaf).obj U ⟶ X') :
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))ᵒᵖ) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.forget_obj
(C : Type u)
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
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' := _}
Instances for algebraic_geometry.PresheafedSpace.forget
- algebraic_geometry.PresheafedSpace.forget.category_theory.limits.preserves_colimits_of_shape
- algebraic_geometry.PresheafedSpace.forget_preserves_colimits
- algebraic_geometry.PresheafedSpace.is_open_immersion.forget_preserves_limits_of_left
- algebraic_geometry.PresheafedSpace.is_open_immersion.forget_preserves_limits_of_right
@[simp]
theorem
algebraic_geometry.PresheafedSpace.forget_map
(C : Type u)
[category_theory.category C]
(X Y : algebraic_geometry.PresheafedSpace C)
(f : X ⟶ Y) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.iso_of_components_hom
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(H : X.carrier ≅ Y.carrier)
(α : H.hom _* X.presheaf ≅ Y.presheaf) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.iso_of_components_inv
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(H : X.carrier ≅ Y.carrier)
(α : H.hom _* X.presheaf ≅ Y.presheaf) :
(algebraic_geometry.PresheafedSpace.iso_of_components H α).inv = {base := H.inv, c := Top.presheaf.to_pushforward_of_iso H α.hom}
def
algebraic_geometry.PresheafedSpace.iso_of_components
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(H : X.carrier ≅ Y.carrier)
(α : H.hom _* X.presheaf ≅ Y.presheaf) :
X ≅ Y
An isomorphism of PresheafedSpaces is a homeomorphism of the underlying space, and a natural transformation between the sheaves.
Equations
- algebraic_geometry.PresheafedSpace.iso_of_components H α = {hom := {base := H.hom, c := α.inv}, inv := {base := H.inv, c := Top.presheaf.to_pushforward_of_iso H α.hom}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
algebraic_geometry.PresheafedSpace.sheaf_iso_of_iso_hom
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(H : X ≅ Y) :
def
algebraic_geometry.PresheafedSpace.sheaf_iso_of_iso
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(H : X ≅ Y) :
Isomorphic PresheafedSpaces have natural isomorphic presheaves.
Equations
- algebraic_geometry.PresheafedSpace.sheaf_iso_of_iso H = {hom := H.hom.c, inv := Top.presheaf.pushforward_to_of_iso ((algebraic_geometry.PresheafedSpace.forget C).map_iso H).symm H.inv.c, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
algebraic_geometry.PresheafedSpace.sheaf_iso_of_iso_inv
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(H : X ≅ Y) :
@[protected, instance]
def
algebraic_geometry.PresheafedSpace.base_is_iso_of_iso
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
@[protected, instance]
def
algebraic_geometry.PresheafedSpace.c_is_iso_of_iso
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(f : X ⟶ Y)
[category_theory.is_iso f] :
theorem
algebraic_geometry.PresheafedSpace.is_iso_of_components
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(f : X ⟶ Y)
[category_theory.is_iso f.base]
[category_theory.is_iso f.c] :
This could be used in conjunction with category_theory.nat_iso.is_iso_of_is_iso_app.
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) :
The restriction of a presheafed space along an open embedding into the space.
@[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) :
@[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) :
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) :
The map from the restriction of a presheafed space.
Equations
- X.of_restrict h = {base := f, c := {app := λ (V : (topological_space.opens ↥(X.carrier))ᵒᵖ), X.presheaf.map (_.adjunction.counit.app (opposite.unop V)).op, naturality' := _}}
Instances for algebraic_geometry.PresheafedSpace.of_restrict
@[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))ᵒᵖ) :
(X.of_restrict h).c.app V = X.presheaf.map (_.adjunction.counit.app (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) :
(X.of_restrict h).base = f
@[protected, instance]
def
algebraic_geometry.PresheafedSpace.of_restrict_mono
{C : Type u}
[category_theory.category C]
{U : Top}
(X : algebraic_geometry.PresheafedSpace C)
(f : U ⟶ X.carrier)
(hf : open_embedding ⇑f) :
category_theory.mono (X.of_restrict hf)
theorem
algebraic_geometry.PresheafedSpace.restrict_top_presheaf
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
theorem
algebraic_geometry.PresheafedSpace.of_restrict_top_c
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
(X.of_restrict _).c = category_theory.eq_to_hom _
def
algebraic_geometry.PresheafedSpace.to_restrict_top
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
The map to the restriction of a presheafed space along the canonical inclusion from the top subspace.
Equations
@[simp]
@[simp]
theorem
algebraic_geometry.PresheafedSpace.to_restrict_top_c
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
def
algebraic_geometry.PresheafedSpace.restrict_top_iso
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
The isomorphism from the restriction to the top subspace.
Equations
- X.restrict_top_iso = {hom := X.of_restrict _, 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 = X.of_restrict _
@[simp]
theorem
algebraic_geometry.PresheafedSpace.restrict_top_iso_inv
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.Γ_obj
{C : Type u}
[category_theory.category C]
(X : (algebraic_geometry.PresheafedSpace C)ᵒᵖ) :
@[simp]
theorem
algebraic_geometry.PresheafedSpace.Γ_map
{C : Type u}
[category_theory.category C]
(X Y : (algebraic_geometry.PresheafedSpace C)ᵒᵖ)
(f : X ⟶ Y) :
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 ⊤), map_id' := _, map_comp' := _}
theorem
algebraic_geometry.PresheafedSpace.Γ_obj_op
{C : Type u}
[category_theory.category C]
(X : algebraic_geometry.PresheafedSpace C) :
theorem
algebraic_geometry.PresheafedSpace.Γ_map_op
{C : Type u}
[category_theory.category C]
{X Y : algebraic_geometry.PresheafedSpace C}
(f : X ⟶ Y) :
def
category_theory.functor.map_presheaf
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(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
@[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) :
@[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) :
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 α ≫ category_theory.eq_to_hom _}, naturality' := _}