mathlib3 documentation

algebraic_geometry.stalks

Stalks for presheaved spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file lifts constructions of stalks and pushforwards of stalks to work with the category of presheafed spaces. Additionally, we prove that restriction of presheafed spaces does not change the stalks.

source
@[reducible]
noncomputable def algebraic_geometry.PresheafedSpace.stalk {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] (X : algebraic_geometry.PresheafedSpace C) (x : ↥X) :
C

The stalk at x of a PresheafedSpace.

source
noncomputable def algebraic_geometry.PresheafedSpace.stalk_map {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (α : X ⟶ Y) (x : ↥X) :
Y.stalk (⇑(α.base) x) ⟶ X.stalk x

A morphism of presheafed spaces induces a morphism of stalks.

Equations
Instances for algebraic_geometry.PresheafedSpace.stalk_map
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.stalk_map_germ {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (α : X ⟶ Y) (U : topological_space.opens ↥(Y.carrier)) (x : ↥((topological_space.opens.map α.base).obj U)) :
Y.presheaf.germ ⟨⇑(α.base) ↑x, _⟩ ≫ algebraic_geometry.PresheafedSpace.stalk_map α ↑x = α.c.app (opposite.op U) ≫ X.presheaf.germ x
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.stalk_map_germ_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (α : X ⟶ Y) (U : topological_space.opens ↥(Y.carrier)) (x : ↥((topological_space.opens.map α.base).obj U)) {X' : C} (f' : X.stalk ↑x ⟶ X') :
Y.presheaf.germ ⟨⇑(α.base) ↑x, _⟩ ≫ algebraic_geometry.PresheafedSpace.stalk_map α ↑x ≫ f' = α.c.app (opposite.op U) ≫ X.presheaf.germ x ≫ f'
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.stalk_map_germ_apply {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (α : X ⟶ Y) (U : topological_space.opens ↥(Y.carrier)) (x : ↥((topological_space.opens.map α.base).obj U)) [I : category_theory.concrete_category C] (x_1 : ↥(Y.presheaf.obj (opposite.op U))) :
⇑(algebraic_geometry.PresheafedSpace.stalk_map α ↑x) (⇑(Y.presheaf.germ ⟨⇑(α.base) ↑x, _⟩) x_1) = ⇑(X.presheaf.germ x) (⇑(α.c.app (opposite.op U)) x_1)
source
noncomputable def algebraic_geometry.PresheafedSpace.restrict_stalk_iso {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : open_embedding ⇑f) (x : ↥U) :
(X.restrict h).stalk x ≅ X.stalk (⇑f x)

For an open embedding f : U ⟶ X and a point x : U, we get an isomorphism between the stalk of X at f x and the stalk of the restriction of X along f at t x.

Equations
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.restrict_stalk_iso_hom_eq_germ_apply {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : open_embedding ⇑f) (V : topological_space.opens ↥U) (x : ↥U) (hx : x ∈ V) [I : category_theory.concrete_category C] (x_1 : ↥((X.restrict h).presheaf.obj (opposite.op V))) :
⇑((X.restrict_stalk_iso h x).hom) (⇑((X.restrict h).presheaf.germ ⟨x, hx⟩) x_1) = ⇑(X.presheaf.germ ⟨⇑f x, _⟩) x_1
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.restrict_stalk_iso_hom_eq_germ {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : open_embedding ⇑f) (V : topological_space.opens ↥U) (x : ↥U) (hx : x ∈ V) :
(X.restrict h).presheaf.germ ⟨x, hx⟩ ≫ (X.restrict_stalk_iso h x).hom = X.presheaf.germ ⟨⇑f x, _⟩
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.restrict_stalk_iso_hom_eq_germ_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : open_embedding ⇑f) (V : topological_space.opens ↥U) (x : ↥U) (hx : x ∈ V) {X' : C} (f' : X.stalk (⇑f x) ⟶ X') :
(X.restrict h).presheaf.germ ⟨x, hx⟩ ≫ (X.restrict_stalk_iso h x).hom ≫ f' = X.presheaf.germ ⟨⇑f x, _⟩ ≫ f'
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.restrict_stalk_iso_inv_eq_germ_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : open_embedding ⇑f) (V : topological_space.opens ↥U) (x : ↥U) (hx : x ∈ V) {X' : C} (f' : (X.restrict h).stalk x ⟶ X') :
X.presheaf.germ ⟨⇑f x, _⟩ ≫ (X.restrict_stalk_iso h x).inv ≫ f' = (X.restrict h).presheaf.germ ⟨x, hx⟩ ≫ f'
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.restrict_stalk_iso_inv_eq_germ_apply {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : open_embedding ⇑f) (V : topological_space.opens ↥U) (x : ↥U) (hx : x ∈ V) [I : category_theory.concrete_category C] (x_1 : ↥(X.presheaf.obj (opposite.op (_.functor.obj V)))) :
⇑((X.restrict_stalk_iso h x).inv) (⇑(X.presheaf.germ ⟨⇑f x, _⟩) x_1) = ⇑((X.restrict h).presheaf.germ ⟨x, hx⟩) x_1
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.restrict_stalk_iso_inv_eq_germ {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : open_embedding ⇑f) (V : topological_space.opens ↥U) (x : ↥U) (hx : x ∈ V) :
X.presheaf.germ ⟨⇑f x, _⟩ ≫ (X.restrict_stalk_iso h x).inv = (X.restrict h).presheaf.germ ⟨x, hx⟩
source
theorem algebraic_geometry.PresheafedSpace.restrict_stalk_iso_inv_eq_of_restrict {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : open_embedding ⇑f) (x : ↥U) :
(X.restrict_stalk_iso h x).inv = algebraic_geometry.PresheafedSpace.stalk_map (X.of_restrict h) x
source
@[protected, instance]
def algebraic_geometry.PresheafedSpace.of_restrict_stalk_map_is_iso {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {U : Top} (X : algebraic_geometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : open_embedding ⇑f) (x : ↥U) :
category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map (X.of_restrict h) x)
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.stalk_map.id {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] (X : algebraic_geometry.PresheafedSpace C) (x : ↥X) :
algebraic_geometry.PresheafedSpace.stalk_map (𝟙 X) x = 𝟙 (X.stalk x)
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.stalk_map.comp {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y Z : algebraic_geometry.PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (x : ↥X) :
algebraic_geometry.PresheafedSpace.stalk_map (α ≫ β) x = algebraic_geometry.PresheafedSpace.stalk_map β (⇑(α.base) x) ≫ algebraic_geometry.PresheafedSpace.stalk_map α x
source
theorem algebraic_geometry.PresheafedSpace.stalk_map.congr {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (α β : X ⟶ Y) (h₁ : α = β) (x x' : ↥X) (h₂ : x = x') :
algebraic_geometry.PresheafedSpace.stalk_map α x ≫ category_theory.eq_to_hom _ = category_theory.eq_to_hom _ ≫ algebraic_geometry.PresheafedSpace.stalk_map β x'

If α = β and x = x', we would like to say that stalk_map α x = stalk_map β x'. Unfortunately, this equality is not well-formed, as their types are not definitionally the same. To get a proper congruence lemma, we therefore have to introduce these eq_to_hom arrows on either side of the equality.

source
theorem algebraic_geometry.PresheafedSpace.stalk_map.congr_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (α β : X ⟶ Y) (h : α = β) (x : ↥X) :
algebraic_geometry.PresheafedSpace.stalk_map α x = category_theory.eq_to_hom _ ≫ algebraic_geometry.PresheafedSpace.stalk_map β x
source
theorem algebraic_geometry.PresheafedSpace.stalk_map.congr_point {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (α : X ⟶ Y) (x x' : ↥X) (h : x = x') :
algebraic_geometry.PresheafedSpace.stalk_map α x ≫ category_theory.eq_to_hom _ = category_theory.eq_to_hom _ ≫ algebraic_geometry.PresheafedSpace.stalk_map α x'
source
@[protected, instance]
def algebraic_geometry.PresheafedSpace.stalk_map.is_iso {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (α : X ⟶ Y) [category_theory.is_iso α] (x : ↥X) :
category_theory.is_iso (algebraic_geometry.PresheafedSpace.stalk_map α x)
source
noncomputable def algebraic_geometry.PresheafedSpace.stalk_map.stalk_iso {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (α : X ≅ Y) (x : ↥X) :
Y.stalk (⇑(α.hom.base) x) ≅ X.stalk x

An isomorphism between presheafed spaces induces an isomorphism of stalks.

Equations
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.stalk_map.stalk_specializes_stalk_map_apply {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↥X} (h : x ⤳ y) [I : category_theory.concrete_category C] (x_1 : ↥(Y.presheaf.stalk (⇑(f.base) y))) :
⇑(algebraic_geometry.PresheafedSpace.stalk_map f x) (⇑(Y.presheaf.stalk_specializes _) x_1) = ⇑(X.presheaf.stalk_specializes h) (⇑(algebraic_geometry.PresheafedSpace.stalk_map f y) x_1)
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.stalk_map.stalk_specializes_stalk_map {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↥X} (h : x ⤳ y) :
Y.presheaf.stalk_specializes _ ≫ algebraic_geometry.PresheafedSpace.stalk_map f x = algebraic_geometry.PresheafedSpace.stalk_map f y ≫ X.presheaf.stalk_specializes h
source
@[simp]
theorem algebraic_geometry.PresheafedSpace.stalk_map.stalk_specializes_stalk_map_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits C] {X Y : algebraic_geometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↥X} (h : x ⤳ y) {X' : C} (f' : X.stalk x ⟶ X') :
Y.presheaf.stalk_specializes _ ≫ algebraic_geometry.PresheafedSpace.stalk_map f x ≫ f' = algebraic_geometry.PresheafedSpace.stalk_map f y ≫ X.presheaf.stalk_specializes h ≫ f'