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 : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : X.Hom Y) (x : ↑↑X) : Y.presheaf.stalk (α.base x) ⟶ X.presheaf.stalk x

A morphism of presheafed spaces induces a morphism of stalks.

Equations

• α.stalkMap x = CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C (α.base x)).map α.c) (TopCat.Presheaf.stalkPushforward C α.base X.presheaf x)

theorem AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : { x : ↑↑X // x ∈ (TopologicalSpace.Opens.map α.base).obj U }) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj (Y.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α ↑x✝) ((Y.presheaf.germ ⟨α.base ↑x✝, ⋯⟩) x) = (X.presheaf.germ x✝) ((α.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 : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : { x : ↑↑X // x ∈ (TopologicalSpace.Opens.map α.base).obj U }) {Z : C} (h : X.presheaf.stalk ↑x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ ⟨α.base ↑x, ⋯⟩) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α ↑x) h) = CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (X.presheaf.germ x) h)

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

theorem AlgebraicGeometry.PresheafedSpace.stalkMap_germ'_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : ↑↑X) (hx : α.base x✝ ∈ U) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj (Y.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x✝) ((Y.presheaf.germ ⟨α.base x✝, hx⟩) x) = (X.presheaf.germ ⟨x✝, hx⟩) ((α.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 : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y) (x : ↑↑X) (hx : α.base x ∈ U) {Z : C} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ ⟨α.base x, hx⟩) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x) h) = CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (X.presheaf.germ ⟨x, hx⟩) h)

@[simp]

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

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

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

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ⇑f) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x✝ ∈ V) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj ((X.restrict h).presheaf.obj (Opposite.op V))) : (X.restrictStalkIso h x✝).hom ((TopCat.Presheaf.germ (⋯.functor.op.comp X.presheaf) ⟨x✝, hx⟩) x) = (X.presheaf.germ ⟨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 : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ⇑f) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {Z : C} (h : X.presheaf.stalk (f x) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.restrict h✝).presheaf.germ ⟨x, hx⟩) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h✝ x).hom h) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ ⟨f x, ⋯⟩) h

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

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ⇑f) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x✝ ∈ V) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj (X.presheaf.obj (Opposite.op (⋯.functor.obj V)))) : (X.restrictStalkIso h x✝).inv ((X.presheaf.germ ⟨f x✝, ⋯⟩) x) = (TopCat.Presheaf.germ (⋯.functor.op.comp X.presheaf) ⟨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 : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ⇑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 ⟨f x, ⋯⟩) (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h✝ x).inv h) = CategoryTheory.CategoryStruct.comp ((X.restrict h✝).presheaf.germ ⟨x, hx⟩) h

@[simp]

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

theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ⇑f) (x : ↑U) : (X.restrictStalkIso h x).inv = AlgebraicGeometry.PresheafedSpace.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 : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X} (h : OpenEmbedding ⇑f) (x : ↑U) : CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (X.ofRestrict h) x)

Equations

• ⋯ = ⋯

@[simp]

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] (X : AlgebraicGeometry.PresheafedSpace C) (x : ↑↑X) : AlgebraicGeometry.PresheafedSpace.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 : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} {Z : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (β : Y ⟶ Z) (x : ↑↑X) : AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (CategoryTheory.CategoryStruct.comp α β) x = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap β (α.base x)) (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α x)

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

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

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

Equations

• ⋯ = ⋯

def AlgebraicGeometry.PresheafedSpace.stalkMap.stalkIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : X ≅ Y) (x : ↑↑X) : Y.presheaf.stalk (α.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)

theorem AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x : ↑↑X} {y : ↑↑X} (h : x ⤳ y) {Z : C} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.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 : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x : ↑↑X} {y : ↑↑X} (h : x✝ ⤳ y) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj (Y.presheaf.stalk (f.base y))) : (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x✝) ((Y.presheaf.stalkSpecializes ⋯) x) = (X.presheaf.stalkSpecializes h) ((AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y) x)

@[simp]

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