Documentation

Mathlib.AlgebraicGeometry.Stalk

Stalks of a Scheme #

Main definitions and results #

noncomputable def AlgebraicGeometry.IsAffineOpen.fromSpecStalk {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {x : X.toPresheafedSpace} (hxU : x U) :
AlgebraicGeometry.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.

Equations
theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (hV : AlgebraicGeometry.IsAffineOpen V) (x : X.toPresheafedSpace) (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 : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
AlgebraicGeometry.Spec (X.presheaf.stalk x) X

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

Equations
  • X.fromSpecStalk x = .fromSpecStalk
noncomputable instance AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
(AlgebraicGeometry.Spec (X.presheaf.stalk x)).Over X
Equations
@[simp]
theorem AlgebraicGeometry.instOverSpecStalkCommRingCatPresheaf_over (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
AlgebraicGeometry.Spec (X.presheaf.stalk x) X = X.fromSpecStalk x
Equations
@[simp]
theorem AlgebraicGeometry.instCanonicallyOver_over (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
AlgebraicGeometry.Spec (X.presheaf.stalk x) X = X.fromSpecStalk x
@[simp]
theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {x : X.toPresheafedSpace} (hxU : x U) :
hU.fromSpecStalk hxU = X.fromSpecStalk x
instance AlgebraicGeometry.IsAffineOpen.fromSpecStalk_isPreimmersion {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) (x : X.toPresheafedSpace) (hx : x U) :
AlgebraicGeometry.IsPreimmersion (hU.fromSpecStalk hx)
Equations
  • =
instance AlgebraicGeometry.instIsPreimmersionFromSpecStalk {X : AlgebraicGeometry.Scheme} (x : X.toPresheafedSpace) :
Equations
  • =
theorem AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (hU : AlgebraicGeometry.IsAffineOpen U) {x : X.toPresheafedSpace} (hxU : x U) :
(hU.fromSpecStalk hxU).base (IsLocalRing.closedPoint (X.presheaf.stalk x)) = x
@[simp]
theorem AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint {X : AlgebraicGeometry.Scheme} {x : X.toPresheafedSpace} :
(X.fromSpecStalk x).base (IsLocalRing.closedPoint (X.presheaf.stalk x)) = x
theorem AlgebraicGeometry.Scheme.fromSpecStalk_app {X : AlgebraicGeometry.Scheme} {U : X.Opens} {x : X.toPresheafedSpace} (hxU : x U) :
AlgebraicGeometry.Scheme.Hom.app (X.fromSpecStalk x) U = CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x hxU) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.stalk x)).inv ((AlgebraicGeometry.Spec (X.presheaf.stalk x)).presheaf.map (CategoryTheory.homOfLE ).op))
@[simp]
theorem AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk {X : AlgebraicGeometry.Scheme} {x y : X.toPresheafedSpace} (h : x y) :
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) (X.fromSpecStalk y) = X.fromSpecStalk x
@[simp]
theorem AlgebraicGeometry.Scheme.Spec_map_stalkSpecializes_fromSpecStalk_assoc {X : AlgebraicGeometry.Scheme} {x y : X.toPresheafedSpace} (h : x y) {Z : AlgebraicGeometry.Scheme} (h✝ : X Z) :
CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.stalkSpecializes h)) (CategoryTheory.CategoryStruct.comp (X.fromSpecStalk y) h✝) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) h✝
Equations
  • =

A variant of Spec_fromSpecStalk that breaks abstraction boundaries.

theorem AlgebraicGeometry.Scheme.range_fromSpecStalk {X : AlgebraicGeometry.Scheme} {x : X.toPresheafedSpace} :
Set.range (X.fromSpecStalk x).base = {y : X.toPresheafedSpace | y x}

Stacks Tag 01J7

noncomputable def AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) :
AlgebraicGeometry.Spec (X.presheaf.stalk x) U

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) :
CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) U = X.fromSpecStalk x
@[simp]
theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_ι_assoc {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) {Z : AlgebraicGeometry.Scheme} (h : X Z) :
instance AlgebraicGeometry.Scheme.instIsOverFromSpecStalkOfMem {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) :
AlgebraicGeometry.Scheme.Hom.IsOver (U.fromSpecStalkOfMem x hxU) X
Equations
  • =
theorem AlgebraicGeometry.Scheme.fromSpecStalk_toSpecΓ (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) X.toSpecΓ = AlgebraicGeometry.Spec.map (X.presheaf.germ x trivial)
@[simp]
theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) :
CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) U.toSpecΓ = AlgebraicGeometry.Spec.map (X.presheaf.germ U x hxU)
@[simp]
theorem AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : X.toPresheafedSpace) (hxU : x U) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)) Z) :

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

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

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.

Equations
  • One or more equations did not get rendered due to their size.
theorem AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk {X : AlgebraicGeometry.Scheme} (x : X.toPresheafedSpace) :
AlgebraicGeometry.Scheme.stalkClosedPointTo (X.fromSpecStalk x) = (X.presheaf.stalkCongr ).hom
theorem AlgebraicGeometry.SpecToEquivOfLocalRing_eq_iff {X : AlgebraicGeometry.Scheme} {R : CommRingCat} {f₁ f₂ : (x : X.toPresheafedSpace) × { f : X.presheaf.stalk x R // IsLocalHom 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 : AlgebraicGeometry.Scheme) (R : CommRingCat) [IsLocalRing R] :
(AlgebraicGeometry.Spec R X) (x : X.toPresheafedSpace) × { f : X.presheaf.stalk x R // IsLocalHom 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.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AlgebraicGeometry.SpecToEquivOfLocalRing_symm_apply (X : AlgebraicGeometry.Scheme) (R : CommRingCat) [IsLocalRing R] (xf : (x : X.toPresheafedSpace) × { f : X.presheaf.stalk x R // IsLocalHom f }) :