The category of locally ringed spaces

We define (bundled) locally ringed spaces (as SheafedSpace CommRing along with the fact that the stalks are local rings), and morphisms between these (morphisms in SheafedSpace with IsLocalHom on the stalk maps).

structure AlgebraicGeometry.LocallyRingedSpaceextends AlgebraicGeometry.SheafedSpace CommRingCat : Type (u + 1)

A LocallyRingedSpace is a topological space equipped with a sheaf of commutative rings such that all the stalks are local rings.

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

• carrier : TopCat
• presheaf : TopCat.Presheaf CommRingCat ↑self.toPresheafedSpace
• IsSheaf : self.presheaf.IsSheaf
• isLocalRing (x : ↑↑self.toPresheafedSpace) : IsLocalRing ↑(self.presheaf.stalk x)

  Stalks of a locally ringed space are local rings.

@[reducible, inline]

abbrev AlgebraicGeometry.LocallyRingedSpace.toRingedSpace (X : LocallyRingedSpace) : RingedSpace

An alias for toSheafedSpace, where the result type is a RingedSpace. This allows us to use dot-notation for the RingedSpace namespace.

def AlgebraicGeometry.LocallyRingedSpace.toTopCat (X : LocallyRingedSpace) : TopCat

The underlying topological space of a locally ringed space.

@[implicit_reducible]

instance AlgebraicGeometry.LocallyRingedSpace.instCoeSortType : CoeSort LocallyRingedSpace (Type u)

instance AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf (X : LocallyRingedSpace) (x : ↑X.toTopCat) : IsLocalRing ↑(X.presheaf.stalk x)

def AlgebraicGeometry.LocallyRingedSpace.𝒪 (X : LocallyRingedSpace) : TopCat.Sheaf CommRingCat X.toTopCat

The structure sheaf of a locally ringed space.

structure AlgebraicGeometry.LocallyRingedSpace.Hom (X Y : LocallyRingedSpace) extends X.Hom Y.toPresheafedSpace : Type u

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

• base : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
• c : Y.presheaf ⟶ (TopCat.Presheaf.pushforward CommRingCat self.base).obj X.presheaf
• prop (x : ↑↑X.toPresheafedSpace) : IsLocalHom (CommRingCat.Hom.hom (self.stalkMap x))

  the underlying morphism induces a local ring homomorphism on stalks

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext {X Y : LocallyRingedSpace} {x y : X.Hom Y} (base : x.base = y.base) (c : x.c ≍ y.c) : x = y

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext_iff {X Y : LocallyRingedSpace} {x y : X.Hom Y} : x = y ↔ x.base = y.base ∧ x.c ≍ y.c

@[reducible, inline]

abbrev AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom {X Y : LocallyRingedSpace} (f : X.Hom Y) : X.toSheafedSpace ⟶ Y.toSheafedSpace

A morphism of locally ringed spaces as a morphism of sheafed spaces.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom_mk {X Y : LocallyRingedSpace} (f : X.Hom Y.toPresheafedSpace) (hf : ∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (f.stalkMap x))) : { toHom := f, prop := hf }.toShHom = CategoryTheory.InducedCategory.homMk f

@[implicit_reducible]

instance AlgebraicGeometry.LocallyRingedSpace.instQuiver : Quiver LocallyRingedSpace

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext' {X Y : LocallyRingedSpace} {f g : X ⟶ Y} (h : f.toHom = g.toHom) : f = g

theorem AlgebraicGeometry.LocallyRingedSpace.Hom.ext'_iff {X Y : LocallyRingedSpace} {f g : X ⟶ Y} : f = g ↔ f.toHom = g.toHom

noncomputable def AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap {X Y : LocallyRingedSpace} (f : X.Hom Y) (x : ↑X.toTopCat) : Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) x) ⟶ X.presheaf.stalk x

A morphism of locally ringed spaces f : X ⟶ Y induces a local ring homomorphism from Y.stalk (f x) to X.stalk x for any x : X.

instance AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : IsLocalHom (CommRingCat.Hom.hom (Hom.stalkMap f x))

instance AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap' {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat) : IsLocalHom (CommRingCat.Hom.hom (f.stalkMap x))

instance AlgebraicGeometry.LocallyRingedSpace.isLocalHomValStalkMap {X Y : LocallyRingedSpace} (f : X.Hom Y) (x : ↑X.toTopCat) : IsLocalHom (CommRingCat.Hom.hom (f.stalkMap x))

def AlgebraicGeometry.LocallyRingedSpace.id (X : LocallyRingedSpace) : X.Hom X

The identity morphism on a locally ringed space.

@[implicit_reducible]

instance AlgebraicGeometry.LocallyRingedSpace.instInhabitedHom (X : LocallyRingedSpace) : Inhabited (X.Hom X)

def AlgebraicGeometry.LocallyRingedSpace.comp {X Y Z : LocallyRingedSpace} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z

Composition of morphisms of locally ringed spaces.

@[implicit_reducible]

instance AlgebraicGeometry.LocallyRingedSpace.instCategory : CategoryTheory.Category.{u, u + 1} LocallyRingedSpace

The category of locally ringed spaces.

def AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace : CategoryTheory.Functor LocallyRingedSpace (SheafedSpace CommRingCat)

The forgetful functor from LocallyRingedSpace to SheafedSpace CommRing.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_map {X✝ Y✝ : LocallyRingedSpace} (f : X✝ ⟶ Y✝) : forgetToSheafedSpace.map f = CategoryTheory.InducedCategory.homMk f.toHom

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace_obj (X : LocallyRingedSpace) : forgetToSheafedSpace.obj X = X.toSheafedSpace

instance AlgebraicGeometry.LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace : forgetToSheafedSpace.Faithful

The canonical map X ⟶ Spec Γ(X, ⊤). This is the unit of the Γ-Spec adjunction.

def AlgebraicGeometry.LocallyRingedSpace.homMk {X Y : LocallyRingedSpace} (f : X.toSheafedSpace ⟶ Y.toSheafedSpace) (h : ∀ (x : ↑X.toTopCat), IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x)) := by infer_instance) : X ⟶ Y

Constructor for morphisms in LocallyRingedSpace.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.homMk_toHom {X Y : LocallyRingedSpace} (f : X.toSheafedSpace ⟶ Y.toSheafedSpace) (h : ∀ (x : ↑X.toTopCat), IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x)) := by infer_instance) : (homMk f h).toHom = f.hom

def AlgebraicGeometry.LocallyRingedSpace.forgetToTop : CategoryTheory.Functor LocallyRingedSpace TopCat

The forgetful functor from LocallyRingedSpace to Top.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.forgetToTop_map {X✝ Y✝ : LocallyRingedSpace} (f : X✝ ⟶ Y✝) : forgetToTop.map f = (SheafedSpace.forget CommRingCat).map (CategoryTheory.InducedCategory.homMk f.toHom)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.forgetToTop_obj (X : LocallyRingedSpace) : forgetToTop.obj X = (SheafedSpace.forget CommRingCat).obj X.toSheafedSpace

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.id_toHom (X : LocallyRingedSpace) : (CategoryTheory.CategoryStruct.id X).toHom = CategoryTheory.CategoryStruct.id X.toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.comp_toHom {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).toHom = CategoryTheory.CategoryStruct.comp f.toHom g.toHom

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.comp_toShHom {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.toShHom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Hom.toShHom f) (Hom.toShHom g)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.id_toShHom' (X : LocallyRingedSpace) : Hom.toShHom (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X.toSheafedSpace

A variant of id_toShHom' that works with 𝟙 X instead of id X.

theorem AlgebraicGeometry.LocallyRingedSpace.comp_base {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

theorem AlgebraicGeometry.LocallyRingedSpace.comp_c {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).c = CategoryTheory.CategoryStruct.comp g.c ((TopCat.Presheaf.pushforward CommRingCat g.base).map f.c)

theorem AlgebraicGeometry.LocallyRingedSpace.comp_c_app {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑Z.toTopCat)ᵒᵖ) : (CategoryTheory.CategoryStruct.comp f g).c.app U = CategoryTheory.CategoryStruct.comp (g.c.app U) (f.c.app (Opposite.op ((TopologicalSpace.Opens.map g.base).obj (Opposite.unop U))))

def AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso {X Y : LocallyRingedSpace} (f : X.toSheafedSpace ⟶ Y.toSheafedSpace) [CategoryTheory.IsIso f] : X ⟶ Y

Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to a morphism X ⟶ Y as locally ringed spaces.

See also isoOfSheafedSpaceIso.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_toHom {X Y : LocallyRingedSpace} (f : X.toSheafedSpace ⟶ Y.toSheafedSpace) [CategoryTheory.IsIso f] : (homOfSheafedSpaceHomOfIsIso f).toHom = f.hom

def AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso {X Y : LocallyRingedSpace} (f : X.toSheafedSpace ≅ Y.toSheafedSpace) : X ≅ Y

Given two locally ringed spaces X and Y, an isomorphism between X and Y as sheafed spaces can be lifted to an isomorphism X ⟶ Y as locally ringed spaces.

This is related to the property that the functor forgetToSheafedSpace reflects isomorphisms. In fact, it is slightly stronger as we do not require f to come from a morphism between locally ringed spaces.

instance AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace : forgetToSheafedSpace.ReflectsIsomorphisms

instance AlgebraicGeometry.LocallyRingedSpace.is_sheafedSpace_iso {X Y : LocallyRingedSpace} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (Hom.toShHom f)

def AlgebraicGeometry.LocallyRingedSpace.restrict {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : LocallyRingedSpace

The restriction of a locally ringed space along an open embedding.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_obj {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (X✝ : (TopologicalSpace.Opens ↑U)ᵒᵖ) : (X.restrict h).presheaf.obj X✝ = X.presheaf.obj (Opposite.op (h.functor.obj (Opposite.unop X✝)))

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrict_carrier {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : ↑(X.restrict h).toPresheafedSpace = U

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrict_presheaf_map {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) {X✝ Y✝ : (TopologicalSpace.Opens ↑U)ᵒᵖ} (f✝ : X✝ ⟶ Y✝) : (X.restrict h).presheaf.map f✝ = X.presheaf.map (h.functor.map f✝.unop).op

def AlgebraicGeometry.LocallyRingedSpace.ofRestrict {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) : X.restrict h ⟶ X

The canonical map from the restriction to the subspace.

def AlgebraicGeometry.LocallyRingedSpace.restrictTopIso (X : LocallyRingedSpace) : X.restrict ⋯ ≅ X

The restriction of a locally ringed space X to the top subspace is isomorphic to X itself.

def AlgebraicGeometry.LocallyRingedSpace.Γ : CategoryTheory.Functor LocallyRingedSpaceᵒᵖ CommRingCat

The global sections, notated Gamma.

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_def : Γ = forgetToSheafedSpace.op.comp SheafedSpace.Γ

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_obj (X : LocallyRingedSpaceᵒᵖ) : Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_obj_op (X : LocallyRingedSpace) : Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map {X Y : LocallyRingedSpaceᵒᵖ} (f : X ⟶ Y) : Γ.map f = f.unop.c.app (Opposite.op ⊤)

theorem AlgebraicGeometry.LocallyRingedSpace.Γ_map_op {X Y : LocallyRingedSpace} (f : X ⟶ Y) : Γ.map f.op = f.c.app (Opposite.op ⊤)

def AlgebraicGeometry.LocallyRingedSpace.empty : LocallyRingedSpace

The empty locally ringed space.

@[implicit_reducible]

instance AlgebraicGeometry.LocallyRingedSpace.instEmptyCollection : EmptyCollection LocallyRingedSpace

def AlgebraicGeometry.LocallyRingedSpace.emptyTo (X : LocallyRingedSpace) : ∅ ⟶ X

The canonical map from the empty locally ringed space.

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.LocallyRingedSpace.instUniqueHomEmptyCollection {X : LocallyRingedSpace} : Unique (∅ ⟶ X)

noncomputable def AlgebraicGeometry.LocallyRingedSpace.emptyIsInitial : CategoryTheory.Limits.IsInitial ∅

The empty space is initial in LocallyRingedSpace.

theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero (X : LocallyRingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : X.toRingedSpace.basicOpen 0 = ⊥

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent (X : LocallyRingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (f : ↑(X.presheaf.obj (Opposite.op U))) (hf : IsNilpotent f) : X.toRingedSpace.basicOpen f = ⊥

instance AlgebraicGeometry.LocallyRingedSpace.component_nontrivial (X : LocallyRingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [hU : Nonempty ↥U] : Nontrivial ↑(X.presheaf.obj (Opposite.op U))

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base {X Y : LocallyRingedSpace} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.hom.base e.inv.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base_apply {X Y : LocallyRingedSpace} (e : X ≅ Y) (x : ↑X.toTopCat) : (CategoryTheory.ConcreteCategory.hom e.inv.base) ((CategoryTheory.ConcreteCategory.hom e.hom.base) x) = x

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base {X Y : LocallyRingedSpace} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.inv.base e.hom.base = CategoryTheory.CategoryStruct.id ↑Y.toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base_apply {X Y : LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat) : (CategoryTheory.ConcreteCategory.hom e.hom.base) ((CategoryTheory.ConcreteCategory.hom e.inv.base) y) = y

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_id (X : LocallyRingedSpace) (x : ↑X.toTopCat) : Hom.stalkMap (CategoryTheory.CategoryStruct.id X) x = CategoryTheory.CategoryStruct.id (X.presheaf.stalk x)

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toTopCat) : Hom.stalkMap (CategoryTheory.CategoryStruct.comp f g) x = CategoryTheory.CategoryStruct.comp (Hom.stalkMap g ((CategoryTheory.ConcreteCategory.hom f.base) x)) (Hom.stalkMap f x)

theorem AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (h : x ⤳ x') : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (Hom.stalkMap f x) = CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x') (X.presheaf.stalkSpecializes h)

theorem AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (h : x ⤳ x') {Z : CommRingCat} (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 x') (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h✝)

theorem AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (h : x ⤳ x') (y : ↑(Y.presheaf.stalk ((TopCat.Hom.hom f.base) x'))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (Hom.stalkMap f x')) y)

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr {X Y : LocallyRingedSpace} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↑X.toTopCat) (hxx' : x = x') : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) (X.presheaf.stalkSpecializes ⋯) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (Hom.stalkMap g x')

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_assoc {X Y : LocallyRingedSpace} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↑X.toTopCat) (hxx' : x = x') {Z : CommRingCat} (h : X.presheaf.stalk x' ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ⋯) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap g x') h)

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom {X Y : LocallyRingedSpace} (f g : X ⟶ Y) (hfg : f = g) (x : ↑X.toTopCat) : Hom.stalkMap f x = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (Hom.stalkMap g x)

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom_assoc {X Y : LocallyRingedSpace} (f g : X ⟶ Y) (hfg : f = g) (x : ↑X.toTopCat) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) h = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap g x) h)

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (hxx' : x = x') : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) (X.presheaf.stalkSpecializes ⋯) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (Hom.stalkMap f x')

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x x' : ↑X.toTopCat) (hxx' : x = x') {Z : CommRingCat} (h : X.presheaf.stalk x' ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ⋯) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x') h)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv {X Y : LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.hom ((CategoryTheory.ConcreteCategory.hom e.inv.base) y)) (Hom.stalkMap e.inv y) = Y.presheaf.stalkSpecializes ⋯

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_assoc {X Y : LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat) {Z : CommRingCat} (h : Y.presheaf.stalk y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.hom ((CategoryTheory.ConcreteCategory.hom e.inv.base) y)) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.inv y) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) h

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply {X Y : LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat) (z : ↑(Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom e.hom.base) ((CategoryTheory.ConcreteCategory.hom e.inv.base) y)))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap e.inv y)) ((CategoryTheory.ConcreteCategory.hom (Hom.stalkMap e.hom ((CategoryTheory.ConcreteCategory.hom e.inv.base) y))) z) = (CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) z

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom {X Y : LocallyRingedSpace} (e : X ≅ Y) (x : ↑X.toTopCat) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.inv ((CategoryTheory.ConcreteCategory.hom e.hom.base) x)) (Hom.stalkMap e.hom x) = X.presheaf.stalkSpecializes ⋯

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_assoc {X Y : LocallyRingedSpace} (e : X ≅ Y) (x : ↑X.toTopCat) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.inv ((CategoryTheory.ConcreteCategory.hom e.hom.base) x)) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.hom x) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes ⋯) h

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply {X Y : LocallyRingedSpace} (e : X ≅ Y) (x : ↑X.toTopCat) (y : ↑(X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom e.inv.base) ((CategoryTheory.ConcreteCategory.hom e.hom.base) x)))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap e.hom x)) ((CategoryTheory.ConcreteCategory.hom (Hom.stalkMap e.inv ((CategoryTheory.ConcreteCategory.hom e.hom.base) x))) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes ⋯)) y

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ {X Y : LocallyRingedSpace} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y.toTopCat) (x : ↑X.toTopCat) (hx : (CategoryTheory.ConcreteCategory.hom f.base) x ∈ U) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) x) hx) (Hom.stalkMap f x) = CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx)

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc {X Y : LocallyRingedSpace} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y.toTopCat) (x : ↑X.toTopCat) (hx : (CategoryTheory.ConcreteCategory.hom f.base) x ∈ U) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) x) hx) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) h) = CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx) h)

theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply {X Y : LocallyRingedSpace} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y.toTopCat) (x : ↑X.toTopCat) (hx : (CategoryTheory.ConcreteCategory.hom f.base) x ∈ U) (y : ↑(Y.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) x) hx)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx)) ((CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op U))) y)

theorem AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen {X Y : LocallyRingedSpace} (f : X ⟶ Y) {U : TopologicalSpace.Opens ↑Y.toTopCat} (s : ↑(Y.presheaf.obj (Opposite.op U))) : (TopologicalSpace.Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) = X.toRingedSpace.basicOpen ((CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op U))) s)

noncomputable def AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (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 x.

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (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 (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_assoc {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {Z : CommRingCat} (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 (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) h✝

theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) (y : ↑((X.restrict h).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).hom) ((CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)) y

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯) (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ V x hx

@[simp]

theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_assoc {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) {Z : CommRingCat} (h✝ : (X.restrict h).presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.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.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U) (hx : x ∈ V) (y : ↑(X.presheaf.obj (Opposite.op (h.functor.obj V)))) : (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).inv) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)) y) = (CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) y

theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : (X.restrictStalkIso h x).inv = Hom.stalkMap (X.ofRestrict h) x

instance AlgebraicGeometry.LocallyRingedSpace.ofRestrict_stalkMap_isIso {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U) : CategoryTheory.IsIso (Hom.stalkMap (X.ofRestrict h) x)