Stalks for presheaved spaces

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.

def AlgebraicGeometry.PresheafedSpace.Hom.stalkMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (α : X.Hom Y) (x : ↑↑X) : Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom α.base) x) ⟶ X.presheaf.stalk x

A morphism of presheafed spaces induces a morphism of stalks.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.PresheafedSpace.stalkMap_germ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : ↑↑X) (hx : (CategoryTheory.ConcreteCategory.hom α.base) x ∈ U) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom α.base) x) hx) (Hom.stalkMap α x) = CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U)) (X.presheaf.germ ((TopologicalSpace.Opens.map α.base).obj U) x hx)

theorem AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : ↑↑X) (hx : (CategoryTheory.ConcreteCategory.hom α.base) x ∈ U) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x✝ : CategoryTheory.ToType (Y.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap α x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom α.base) x) hx)) x✝) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ((TopologicalSpace.Opens.map α.base).obj U) x hx)) ((CategoryTheory.ConcreteCategory.hom (α.c.app (Opposite.op U))) x✝)

theorem AlgebraicGeometry.PresheafedSpace.stalkMap_germ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : ↑↑X) (hx : (CategoryTheory.ConcreteCategory.hom α.base) x ∈ U) {Z : C} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom α.base) x) hx) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap α x) h) = CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((TopologicalSpace.Opens.map α.base).obj U) x hx) h)

def AlgebraicGeometry.PresheafedSpace.restrictStalkIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : (X.restrict h).presheaf.stalk x ≅ X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom 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

• X.restrictStalkIso h x = CategoryTheory.Functor.Final.colimitIso (⋯.functorNhds x).op ((TopologicalSpace.OpenNhds.inclusion ((CategoryTheory.ConcreteCategory.hom f) x)).op.comp X.presheaf)

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) (X.restrictStalkIso h x).hom = X.presheaf.germ (⋯.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x✝ : CategoryTheory.ToType ((X.restrict h).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).hom) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ (⋯.functor.op.comp X.presheaf) V x hx)) x✝) = (X.presheaf.germ (⋯.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) x✝

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {Z : C} (h✝ : X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).hom h✝) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ (⋯.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) h✝

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ (⋯.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ V x hx

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x✝ : CategoryTheory.ToType (X.presheaf.obj (Opposite.op (⋯.functor.obj V)))) : (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).inv) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (⋯.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)) x✝) = (TopCat.Presheaf.germ (⋯.functor.op.comp X.presheaf) V x hx) x✝

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {Z : C} (h✝ : (X.restrict h).presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ (⋯.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).inv h✝) = CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) h✝

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : (X.restrictStalkIso h x).inv = Hom.stalkMap (X.ofRestrict h) x

instance AlgebraicGeometry.PresheafedSpace.ofRestrict_stalkMap_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : PresheafedSpace C) {f : U ⟶ ↑X} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : CategoryTheory.IsIso (Hom.stalkMap (X.ofRestrict h) x)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] (X : PresheafedSpace C) (x : ↑↑X) : Hom.stalkMap (CategoryTheory.CategoryStruct.id X) x = CategoryTheory.CategoryStruct.id (X.presheaf.stalk x)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y Z : PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (x : ↑↑X) : Hom.stalkMap (CategoryTheory.CategoryStruct.comp α β) x = CategoryTheory.CategoryStruct.comp (Hom.stalkMap β ((CategoryTheory.ConcreteCategory.hom α.base) x)) (Hom.stalkMap α x)

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (α β : X ⟶ Y) (h₁ : α = β) (x x' : ↑↑X) (h₂ : x = x') : CategoryTheory.CategoryStruct.comp (Hom.stalkMap α x) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (Hom.stalkMap β 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 eqToHom arrows on either side of the equality.

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (α β : X ⟶ Y) (h : α = β) (x : ↑↑X) : Hom.stalkMap α x = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (Hom.stalkMap β x)

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.congr_point {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (α : X ⟶ Y) (x x' : ↑↑X) (h : x = x') : CategoryTheory.CategoryStruct.comp (Hom.stalkMap α x) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (Hom.stalkMap α x')

instance AlgebraicGeometry.PresheafedSpace.stalkMap.isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (α : X ⟶ Y) [CategoryTheory.IsIso α] (x : ↑↑X) : CategoryTheory.IsIso (Hom.stalkMap α x)

def AlgebraicGeometry.PresheafedSpace.stalkMap.stalkIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (α : X ≅ Y) (x : ↑↑X) : Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom α.hom.base) x) ≅ X.presheaf.stalk x

An isomorphism between presheafed spaces induces an isomorphism of stalks.

Equations

• AlgebraicGeometry.PresheafedSpace.stalkMap.stalkIso α x = CategoryTheory.asIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α.hom x)

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (Hom.stalkMap f x) = CategoryTheory.CategoryStruct.comp (Hom.stalkMap f y) (X.presheaf.stalkSpecializes h)

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y) {Z : C} (h✝ : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) h✝) = CategoryTheory.CategoryStruct.comp (Hom.stalkMap f y) (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h✝)

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X Y : PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y) {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F] (x✝ : CategoryTheory.ToType (Y.presheaf.stalk ((TopCat.Hom.hom f.base) y))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) x✝) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (Hom.stalkMap f y)) x✝)