Stalks of a Scheme

Main definitions and results

• AlgebraicGeometry.Scheme.fromSpecStalk: The canonical morphism Spec 𝒪_{X, x} ⟶ X.
• AlgebraicGeometry.Scheme.range_fromSpecStalk: The range of the map Spec 𝒪_{X, x} ⟶ X is exactly the ys that specialize to x.
• AlgebraicGeometry.SpecToEquivOfLocalRing: Given a local ring R and scheme X, morphisms Spec R ⟶ X corresponds to pairs (x, f) where x : X and f : 𝒪_{X, x} ⟶ R is a local ring homomorphism.

noncomputable def AlgebraicGeometry.IsAffineOpen.fromSpecStalk {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {x : ↥X} (hxU : x ∈ U) : Spec (X.presheaf.stalk x) ⟶ X

A morphism from Spec(O_x) to X, which is defined with the help of an affine open neighborhood U of x.

theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq {X : Scheme} {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (x : ↥X) (hxU : x ∈ U) (hxV : x ∈ V) : hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

The morphism from Spec(O_x) to X given by IsAffineOpen.fromSpec does not depend on the affine open neighborhood of x we choose.

noncomputable def AlgebraicGeometry.Scheme.fromSpecStalk (X : Scheme) (x : ↥X) : Spec (X.presheaf.stalk x) ⟶ X

If x is a point of X, this is the canonical morphism from Spec(O_x) to X.

noncomputable instance AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf (X : Scheme) (x : ↥X) : (Spec (X.presheaf.stalk x)).Over X

@[simp]

theorem AlgebraicGeometry.over_def (X : Scheme) (x : ↥X) : Spec (X.presheaf.stalk x) ↘ X = X.fromSpecStalk x

noncomputable instance AlgebraicGeometry.instCanonicallyOverSpecStalkCommRingCatPresheaf (X : Scheme) (x : ↥X) : (Spec (X.presheaf.stalk x)).CanonicallyOver X

@[simp]

theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {x : ↥X} (hxU : x ∈ U) : hU.fromSpecStalk hxU = X.fromSpecStalk x

instance AlgebraicGeometry.IsAffineOpen.fromSpecStalk_isPreimmersion {X : Scheme} {U : TopologicalSpace.Opens ↥X} (hU : IsAffineOpen U) (x : ↥X) (hx : x ∈ U) : IsPreimmersion (hU.fromSpecStalk hx)

instance AlgebraicGeometry.instIsPreimmersionFromSpecStalk {X : Scheme} (x : ↥X) : IsPreimmersion (X.fromSpecStalk x)

theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint {X : Scheme} {U : TopologicalSpace.Opens ↥X} (hU : IsAffineOpen U) {x : ↥X} (hxU : x ∈ U) : (CategoryTheory.ConcreteCategory.hom (hU.fromSpecStalk hxU).base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) = x

@[simp]

theorem AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint {X : Scheme} {x : ↥X} : (CategoryTheory.ConcreteCategory.hom (X.fromSpecStalk x).base) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) = x

theorem AlgebraicGeometry.Scheme.fromSpecStalk_app {X : Scheme} {U : X.Opens} {x : ↥X} (hxU : x ∈ U) : Hom.app (X.fromSpecStalk x) U = CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x hxU) (CategoryTheory.CategoryStruct.comp (ΓSpecIso (X.presheaf.stalk x)).inv ((Spec (X.presheaf.stalk x)).presheaf.map (CategoryTheory.homOfLE ⋯).op))

theorem AlgebraicGeometry.Scheme.fromSpecStalk_appTop {X : Scheme} {x : ↥X} : Hom.appTop (X.fromSpecStalk x) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ ⊤ x trivial) (CategoryTheory.CategoryStruct.comp (ΓSpecIso (X.presheaf.stalk x)).inv ((Spec (X.presheaf.stalk x)).presheaf.map (CategoryTheory.homOfLE ⋯).op))

@[simp]

theorem AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk {X : Scheme} {x y : ↥X} (h : x ⤳ y) : CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.stalkSpecializes h)) (X.fromSpecStalk y) = X.fromSpecStalk x

@[simp]

theorem AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc {X : Scheme} {x y : ↥X} (h : x ⤳ y) {Z : Scheme} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.stalkSpecializes h)) (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk y) h✝) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) h✝

instance AlgebraicGeometry.Scheme.instIsOverMapStalkSpecializesCommRingCatPresheaf {X : Scheme} {x y : ↥X} (h : x ⤳ y) : Hom.IsOver (Spec.map (X.presheaf.stalkSpecializes h)) X

@[simp]

theorem AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk {X Y : Scheme} (f : X ⟶ Y) {x : ↥X} : CategoryTheory.CategoryStruct.comp (Spec.map (Hom.stalkMap f x)) (Y.fromSpecStalk ((CategoryTheory.ConcreteCategory.hom f.base) x)) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f

@[simp]

theorem AlgebraicGeometry.Scheme.Spec_map_stalkMap_fromSpecStalk_assoc {X Y : Scheme} (f : X ⟶ Y) {x : ↥X} {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (Hom.stalkMap f x)) (CategoryTheory.CategoryStruct.comp (Y.fromSpecStalk ((CategoryTheory.ConcreteCategory.hom f.base) x)) h) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) (CategoryTheory.CategoryStruct.comp f h)

instance AlgebraicGeometry.Scheme.instIsOverMapStalkMapOverInferInstanceOverClass {X Y : Scheme} [X.Over Y] {x : ↥X} : Hom.IsOver (Spec.map (Hom.stalkMap (X ↘ Y) x)) Y

theorem AlgebraicGeometry.Scheme.Spec_fromSpecStalk (R : CommRingCat) (x : ↥(Spec R)) : (Spec R).fromSpecStalk x = Spec.map (CategoryTheory.CategoryStruct.comp (ΓSpecIso R).inv ((Spec R).presheaf.germ ⊤ x trivial))

theorem AlgebraicGeometry.Scheme.Spec_fromSpecStalk' (R : CommRingCat) (x : ↥(Spec R)) : (Spec R).fromSpecStalk x = Spec.map (StructureSheaf.toStalk (↑R) x)

A variant of Spec_fromSpecStalk that breaks abstraction boundaries.

theorem AlgebraicGeometry.Scheme.range_fromSpecStalk {X : Scheme} {x : ↥X} : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (X.fromSpecStalk x).base) = {y : ↥X | y ⤳ x}

Stacks Tag 01J7

noncomputable def AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem {X : Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U) : Spec (X.presheaf.stalk x) ⟶ ↑U

The canonical map Spec 𝒪_{X, x} ⟶ U given x ∈ U ⊆ X.

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι {X : Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U) : CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) U.ι = X.fromSpecStalk x

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι_assoc {X : Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) (CategoryTheory.CategoryStruct.comp U.ι h) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) h

instance AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem {X : Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U) : Hom.IsOver (U.fromSpecStalkOfMem x hxU) X

theorem AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ (X : Scheme) (x : ↥X) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) X.toSpecΓ = Spec.map (X.presheaf.germ ⊤ x trivial)

theorem AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ_assoc (X : Scheme) (x : ↥X) {Z : Scheme} (h : Spec (X.presheaf.obj (Opposite.op ⊤)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) (CategoryTheory.CategoryStruct.comp X.toSpecΓ h) = CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.germ ⊤ x trivial)) h

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ {X : Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U) : CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) U.toSpecΓ = Spec.map (X.presheaf.germ U x hxU)

@[simp]

theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc {X : Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U) {Z : Scheme} (h : Spec (X.presheaf.obj (Opposite.op U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) (CategoryTheory.CategoryStruct.comp U.toSpecΓ h) = CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.germ U x hxU)) h

noncomputable def AlgebraicGeometry.stalkClosedPointIso (R : CommRingCat) [IsLocalRing ↑R] : (Spec R).presheaf.stalk (IsLocalRing.closedPoint ↑R) ≅ R

For a local ring (R, 𝔪), this is the isomorphism between the stalk of Spec R at 𝔪 and R.

theorem AlgebraicGeometry.stalkClosedPointIso_inv (R : CommRingCat) [IsLocalRing ↑R] : (stalkClosedPointIso R).inv = StructureSheaf.toStalk (↑R) (IsLocalRing.closedPoint ↑R)

theorem AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv (R : CommRingCat) [IsLocalRing ↑R] : CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso R).hom (stalkClosedPointIso R).inv = (Spec R).presheaf.germ ⊤ (IsLocalRing.closedPoint ↑R) trivial

@[simp]

theorem AlgebraicGeometry.germ_stalkClosedPointIso_hom (R : CommRingCat) [IsLocalRing ↑R] : CategoryTheory.CategoryStruct.comp ((Spec R).presheaf.germ ⊤ (IsLocalRing.closedPoint ↑R) trivial) (stalkClosedPointIso R).hom = (Scheme.ΓSpecIso R).hom

@[simp]

theorem AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc (R : CommRingCat) [IsLocalRing ↑R] {Z : CommRingCat} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp ((Spec R).presheaf.germ ⊤ (IsLocalRing.closedPoint ↑R) trivial) (CategoryTheory.CategoryStruct.comp (stalkClosedPointIso R).hom h) = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso R).hom h

theorem AlgebraicGeometry.Spec_stalkClosedPointIso (R : CommRingCat) [IsLocalRing ↑R] : Spec.map (stalkClosedPointIso R).inv = (Spec R).fromSpecStalk (IsLocalRing.closedPoint ↑R)

noncomputable def AlgebraicGeometry.Scheme.stalkClosedPointTo {X : Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : Spec R ⟶ X) : X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R)) ⟶ R

Given a local ring (R, 𝔪) and a morphism f : Spec R ⟶ X, they induce a (local) ring homomorphism φ : 𝒪_{X, f 𝔪} ⟶ R.

This is inverse to φ ↦ Spec.map φ ≫ X.fromSpecStalk (f 𝔪). See SpecToEquivOfLocalRing.

instance AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo {X : Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : Spec R ⟶ X) : IsLocalHom (CommRingCat.Hom.hom (stalkClosedPointTo f))

instance AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo' {X : Scheme} {R : Type u} [CommRing R] [IsLocalRing R] (f : Spec (CommRingCat.of R) ⟶ X) : IsLocalHom (CommRingCat.Hom.hom (stalkClosedPointTo f))

Copy of isLocalHom_stalkClosedPointTo which unbundles the comm ring.

Useful for use in combination with CommRingCat.of K for a field K.

theorem AlgebraicGeometry.Scheme.preimage_eq_top_of_closedPoint_mem {X : Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : Spec R ⟶ X) {U : X.Opens} (hU : (CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R) ∈ U) : (TopologicalSpace.Opens.map f.base).obj U = ⊤

theorem AlgebraicGeometry.Scheme.stalkClosedPointTo_comp {X Y : Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : Spec R ⟶ X) (g : X ⟶ Y) : stalkClosedPointTo (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Hom.stalkMap g ((CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R))) (stalkClosedPointTo f)

theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec {R S : CommRingCat} [IsLocalRing ↑S] (φ : R ⟶ S) : CategoryTheory.CategoryStruct.comp ((Spec R).presheaf.germ ⊤ ((CategoryTheory.ConcreteCategory.hom (Spec.map φ).base) (IsLocalRing.closedPoint ↑S)) trivial) (stalkClosedPointTo (Spec.map φ)) = CategoryTheory.CategoryStruct.comp (ΓSpecIso R).hom φ

theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo {X : Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : Spec R ⟶ X) (U : X.Opens) (hU : (CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R) ∈ U) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R)) hU) (stalkClosedPointTo f) = CategoryTheory.CategoryStruct.comp (Hom.app f U) (CategoryTheory.Functor.mapIso (Spec R).presheaf (CategoryTheory.eqToIso ⋯).op ≪≫ ΓSpecIso R).hom

theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_assoc {X : Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : Spec R ⟶ X) (U : X.Opens) (hU : (CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R) ∈ U) {Z : CommRingCat} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R)) hU) (CategoryTheory.CategoryStruct.comp (stalkClosedPointTo f) h) = CategoryTheory.CategoryStruct.comp (Hom.app f U) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapIso (Spec R).presheaf (CategoryTheory.eqToIso ⋯).op ≪≫ ΓSpecIso R).hom h)

theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk {X : Scheme} {R : CommRingCat} [IsLocalRing ↑R] {x : ↥X} (f : X.presheaf.stalk x ⟶ R) [IsLocalHom (CommRingCat.Hom.hom f)] (U : X.Opens) (hU : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (Spec.map f) (X.fromSpecStalk x)).base) (IsLocalRing.closedPoint ↑R) ∈ U) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (Spec.map f) (X.fromSpecStalk x)).base) (IsLocalRing.closedPoint ↑R)) hU) (stalkClosedPointTo (CategoryTheory.CategoryStruct.comp (Spec.map f) (X.fromSpecStalk x))) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x ⋯) f

theorem AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk_assoc {X : Scheme} {R : CommRingCat} [IsLocalRing ↑R] {x : ↥X} (f : X.presheaf.stalk x ⟶ R) [IsLocalHom (CommRingCat.Hom.hom f)] (U : X.Opens) (hU : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (Spec.map f) (X.fromSpecStalk x)).base) (IsLocalRing.closedPoint ↑R) ∈ U) {Z : CommRingCat} (h : R ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (Spec.map f) (X.fromSpecStalk x)).base) (IsLocalRing.closedPoint ↑R)) hU) (CategoryTheory.CategoryStruct.comp (stalkClosedPointTo (CategoryTheory.CategoryStruct.comp (Spec.map f) (X.fromSpecStalk x))) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x ⋯) (CategoryTheory.CategoryStruct.comp f h)

theorem AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk {X : Scheme} (x : ↥X) : stalkClosedPointTo (X.fromSpecStalk x) = (X.presheaf.stalkCongr ⋯).hom

theorem AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk {X : Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : Spec R ⟶ X) : CategoryTheory.CategoryStruct.comp (Spec.map (stalkClosedPointTo f)) (X.fromSpecStalk ((CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R))) = f

theorem AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc {X : Scheme} {R : CommRingCat} [IsLocalRing ↑R] (f : Spec R ⟶ X) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (stalkClosedPointTo f)) (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk ((CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R))) h) = CategoryTheory.CategoryStruct.comp f h

theorem AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff {X : Scheme} {R : CommRingCat} {f₁ f₂ : (x : ↥X) × { f : X.presheaf.stalk x ⟶ R // IsLocalHom (CommRingCat.Hom.hom f) }} : f₁ = f₂ ↔ ∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom ↑f₂.snd

useful lemma for applications of SpecToEquivOfLocalRing

noncomputable def AlgebraicGeometry.SpecToEquivOfLocalRing (X : Scheme) (R : CommRingCat) [IsLocalRing ↑R] : (Spec R ⟶ X) ≃ (x : ↥X) × { f : X.presheaf.stalk x ⟶ R // IsLocalHom (CommRingCat.Hom.hom f) }

Given a local ring R and scheme X, morphisms Spec R ⟶ X corresponds to pairs (x, f) where x : X and f : 𝒪_{X, x} ⟶ R is a local ring homomorphism.

@[simp]

theorem AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst (X : Scheme) (R : CommRingCat) [IsLocalRing ↑R] (f : Spec R ⟶ X) : ((SpecToEquivOfLocalRing X R) f).fst = (CategoryTheory.ConcreteCategory.hom f.base) (IsLocalRing.closedPoint ↑R)

@[simp]

theorem AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe (X : Scheme) (R : CommRingCat) [IsLocalRing ↑R] (f : Spec R ⟶ X) : ↑((SpecToEquivOfLocalRing X R) f).snd = Scheme.stalkClosedPointTo f

@[simp]

theorem AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply (X : Scheme) (R : CommRingCat) [IsLocalRing ↑R] (xf : (x : ↥X) × { f : X.presheaf.stalk x ⟶ R // IsLocalHom (CommRingCat.Hom.hom f) }) : (SpecToEquivOfLocalRing X R).symm xf = CategoryTheory.CategoryStruct.comp (Spec.map ↑xf.snd) (X.fromSpecStalk xf.fst)