Module

StalkLocalization.lean

Nyll.SchemeTheory.Affine.StalkLocalization

6 declarations indexed from sourceView source ↗

Module documentation

Stalks of localization morphisms

The canonical map from the spectrum of an arbitrary model of a localization has isomorphic stalk maps. Mathlib contains this for the quotient-type Localization M; the statement below removes that representation choice.

Imports5

Mathlib.AlgebraicGeometry.Stalk
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.RingTheory.Ideal.Height
Mathlib.RingTheory.Localization.LocalizationLocalization

Imported by8

theorem

isIso_stalkMap_SpecMap_of_isLocalization

L31 ↗

AlgebraicGeometry.isIso_stalkMap_SpecMap_of_isLocalization

Documentation

The stalk map of Spec S ⟶ Spec R is an isomorphism when S is a localization of R, independently of the chosen localization model.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem isIso_stalkMap_SpecMap_of_isLocalization
    {R S : CommRingCat.{u}} (M : Submonoid R)
    [Algebra R S] [IsLocalization M S]
    (x : PrimeSpectrum S) :
    IsIso ((Spec.map (CommRingCat.ofHom (algebraMap R S))).stalkMap x)

theorem

isIso_fromSpecStalk_stalkMap

L65 ↗

AlgebraicGeometry.IsAffineOpen.isIso_fromSpecStalk_stalkMap

Documentation

Every stalk map of the canonical morphism from the spectrum of a stalk, computed inside a chosen affine neighbourhood, is an isomorphism.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem IsAffineOpen.isIso_fromSpecStalk_stalkMap
    {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U)
    (x : X) (hx : x ∈ U) (p : PrimeSpectrum (X.presheaf.stalk x)) :
    IsIso ((hU.fromSpecStalk hx).stalkMap p)

theorem

isIso_fromSpecStalk_stalkMap

L87 ↗

AlgebraicGeometry.Scheme.isIso_fromSpecStalk_stalkMap

Documentation

Every stalk map of the canonical morphism Spec 𝒪_{X,x} ⟶ X is an isomorphism. Equivalently, the local ring at a generalization of x is the corresponding prime localization of 𝒪_{X,x}.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem Scheme.isIso_fromSpecStalk_stalkMap
    (X : Scheme.{u}) (x : X) (p : PrimeSpectrum (X.presheaf.stalk x)) :
    IsIso ((X.fromSpecStalk x).stalkMap p)

def

stalkFromSpecStalkEquivLocalization

L99 ↗

AlgebraicGeometry.Scheme.stalkFromSpecStalkEquivLocalization

Documentation

The local ring at the image of a prime of 𝒪_{X,x} is canonically isomorphic to the localization of 𝒪_{X,x} at that prime.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

def Scheme.stalkFromSpecStalkEquivLocalization
    (X : Scheme.{u}) (x : X) (p : PrimeSpectrum (X.presheaf.stalk x)) :
    X.presheaf.stalk (X.fromSpecStalk x p) ≃+*
      Localization.AtPrime p.asIdeal

theorem

ringKrullDim_stalk_fromSpecStalk_eq_height

L109 ↗

AlgebraicGeometry.Scheme.ringKrullDim_stalk_fromSpecStalk_eq_height

Documentation

The dimension of the local ring at the point represented by p in Spec 𝒪_{X,x} is the height of p.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem Scheme.ringKrullDim_stalk_fromSpecStalk_eq_height
    (X : Scheme.{u}) (x : X) (p : PrimeSpectrum (X.presheaf.stalk x)) :
    ringKrullDim (X.presheaf.stalk (X.fromSpecStalk x p)) =
      p.asIdeal.height

def

residueFieldFromSpecStalkEquiv

L120 ↗

AlgebraicGeometry.Scheme.residueFieldFromSpecStalkEquiv

Documentation

The residue field at a point represented in the spectrum of a stalk is canonically the residue field of the corresponding prime of that stalk.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

def Scheme.residueFieldFromSpecStalkEquiv
    (X : Scheme.{u}) (x : X) (p : PrimeSpectrum (X.presheaf.stalk x)) :
    X.residueField (X.fromSpecStalk x p) ≃+* p.asIdeal.ResidueField

Module documentation

Stalks of localization morphisms

Declarations

isIso_stalkMap_SpecMap_of_isLocalization

isIso_fromSpecStalk_stalkMap

isIso_fromSpecStalk_stalkMap

stalkFromSpecStalkEquivLocalization

ringKrullDim_stalk_fromSpecStalk_eq_height

residueFieldFromSpecStalkEquiv