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.

@[inline, reducible]

abbrev AlgebraicGeometry.PresheafedSpace.stalk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] (X : AlgebraicGeometry.PresheafedSpace C) (x : ↑↑X) : C

The stalk at x of a PresheafedSpace.

Equations

• AlgebraicGeometry.PresheafedSpace.stalk X x = TopCat.Presheaf.stalk X.presheaf x

def AlgebraicGeometry.PresheafedSpace.stalkMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimits C] {X : AlgebraicGeometry.PresheafedSpace C} {Y : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y) (x : ↑↑X) : AlgebraicGeometry.PresheafedSpace.stalk Y (α.base x) ⟶ AlgebraicGeometry.PresheafedSpace.stalk X 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_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 : ↥((TopologicalSpace.Opens.map α.base).obj U)) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj (Y.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.PresheafedSpace.stalkMap α ↑x✝) ((TopCat.Presheaf.germ Y.presheaf { val := α.base ↑x✝, property := ⋯ }) x) = (TopCat.Presheaf.germ X.presheaf 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 : ↥((TopologicalSpace.Opens.map α.base).obj U)) {Z : C} (h : AlgebraicGeometry.PresheafedSpace.stalk X ↑x ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ Y.presheaf { val := α.base ↑x, property := ⋯ }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.stalkMap α ↑x) h) = CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ X.presheaf 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 : ↥((TopologicalSpace.Opens.map α.base).obj U)) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ Y.presheaf { val := α.base ↑x, property := ⋯ }) (AlgebraicGeometry.PresheafedSpace.stalkMap α ↑x) = CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U)) (TopCat.Presheaf.germ 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) (hx : α.base x✝ ∈ U) [inst : CategoryTheory.ConcreteCategory C] (x : (CategoryTheory.forget C).obj (Y.presheaf.obj (Opposite.op U))) : (AlgebraicGeometry.PresheafedSpace.stalkMap α x✝) ((TopCat.Presheaf.germ Y.presheaf { val := α.base x✝, property := hx }) x) = (TopCat.Presheaf.germ X.presheaf { val := x✝, property := 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 : AlgebraicGeometry.PresheafedSpace.stalk X x ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ Y.presheaf { val := α.base x, property := hx }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.stalkMap α x) h) = CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ X.presheaf { val := x, property := 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 (TopCat.Presheaf.germ Y.presheaf { val := α.base x, property := hx }) (AlgebraicGeometry.PresheafedSpace.stalkMap α x) = CategoryTheory.CategoryStruct.comp (α.c.app (Opposite.op U)) (TopCat.Presheaf.germ X.presheaf { val := x, property := 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) : AlgebraicGeometry.PresheafedSpace.stalk (AlgebraicGeometry.PresheafedSpace.restrict X h) x ≅ AlgebraicGeometry.PresheafedSpace.stalk X (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

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

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 ((CategoryTheory.Functor.comp (IsOpenMap.functorNhds ⋯ x✝).op (CategoryTheory.Functor.comp (TopologicalSpace.OpenNhds.inclusion (f x✝)).op X.presheaf)).obj (Opposite.op { obj := V, property := hx }))) : (CategoryTheory.Limits.colimit.pre (CategoryTheory.Functor.comp (TopologicalSpace.OpenNhds.inclusion (f x✝)).op X.presheaf) (IsOpenMap.functorNhds ⋯ x✝).op) ((CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (IsOpenMap.functorNhds ⋯ x✝).op (CategoryTheory.Functor.comp (TopologicalSpace.OpenNhds.inclusion (f x✝)).op X.presheaf)) (Opposite.op { obj := V, property := hx })) x) = (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.comp (TopologicalSpace.OpenNhds.inclusion (f x✝)).op X.presheaf) (Opposite.op ((IsOpenMap.functorNhds ⋯ x✝).obj { obj := V, property := hx }))) 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 : AlgebraicGeometry.PresheafedSpace.stalk X (f x) ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ (AlgebraicGeometry.PresheafedSpace.restrict X h✝).presheaf { val := x, property := hx }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.restrictStalkIso X h✝ x).hom h) = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ X.presheaf { val := f x, property := ⋯ }) 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 (TopCat.Presheaf.germ (AlgebraicGeometry.PresheafedSpace.restrict X h).presheaf { val := x, property := hx }) (AlgebraicGeometry.PresheafedSpace.restrictStalkIso X h x).hom = TopCat.Presheaf.germ X.presheaf { val := f x, property := ⋯ }

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 ((IsOpenMap.functor ⋯).obj V)))) : (AlgebraicGeometry.PresheafedSpace.restrictStalkIso X h x✝).inv ((TopCat.Presheaf.germ X.presheaf { val := f x✝, property := ⋯ }) x) = (TopCat.Presheaf.germ (CategoryTheory.Functor.comp (IsOpenMap.functor ⋯).op X.presheaf) { val := x✝, property := 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 : AlgebraicGeometry.PresheafedSpace.stalk (AlgebraicGeometry.PresheafedSpace.restrict X h✝) x ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ X.presheaf { val := f x, property := ⋯ }) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.restrictStalkIso X h✝ x).inv h) = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ (AlgebraicGeometry.PresheafedSpace.restrict X h✝).presheaf { val := x, property := 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 (TopCat.Presheaf.germ X.presheaf { val := f x, property := ⋯ }) (AlgebraicGeometry.PresheafedSpace.restrictStalkIso X h x).inv = TopCat.Presheaf.germ (AlgebraicGeometry.PresheafedSpace.restrict X h).presheaf { val := x, property := 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) : (AlgebraicGeometry.PresheafedSpace.restrictStalkIso X h x).inv = AlgebraicGeometry.PresheafedSpace.stalkMap (AlgebraicGeometry.PresheafedSpace.ofRestrict X 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.stalkMap (AlgebraicGeometry.PresheafedSpace.ofRestrict X 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.stalkMap (CategoryTheory.CategoryStruct.id X) x = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.PresheafedSpace.stalk X 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.stalkMap (CategoryTheory.CategoryStruct.comp α β) x = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.stalkMap β (α.base x)) (AlgebraicGeometry.PresheafedSpace.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.stalkMap α x) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.PresheafedSpace.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 eq_to_hom 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.stalkMap α x = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.PresheafedSpace.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.stalkMap α x) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.PresheafedSpace.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.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) : AlgebraicGeometry.PresheafedSpace.stalk Y (α.hom.base x) ≅ AlgebraicGeometry.PresheafedSpace.stalk X x

An isomorphism between presheafed spaces induces an isomorphism of stalks.

Equations

• AlgebraicGeometry.PresheafedSpace.stalkMap.stalkIso α x = CategoryTheory.asIso (AlgebraicGeometry.PresheafedSpace.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 : AlgebraicGeometry.PresheafedSpace.stalk X x ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkSpecializes Y.presheaf ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.stalkMap f x) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.stalkMap f y) (CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.stalkSpecializes X.presheaf 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 (TopCat.Presheaf.stalk Y.presheaf (f.base y))) : (AlgebraicGeometry.PresheafedSpace.stalkMap f x✝) ((TopCat.Presheaf.stalkSpecializes Y.presheaf ⋯) x) = (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.stalkMap f y) (TopCat.Presheaf.stalkSpecializes X.presheaf h)) 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 (TopCat.Presheaf.stalkSpecializes Y.presheaf ⋯) (AlgebraicGeometry.PresheafedSpace.stalkMap f x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.stalkMap f y) (TopCat.Presheaf.stalkSpecializes X.presheaf h)