NYLL
Module

LocalScheme.lean

Nyll.SchemeTheory.Divisors.LocalScheme
2 declarations indexed from sourceView source ↗

Module documentation

Divisors on spectra of local rings

This file relates the support of an ideal sheaf near a scheme point to prime ideals of its local ring. It contains the point-level bridge used when a codimension-two localization is selected inside a local ramification argument.

Imports7
Imported by4

Declarations

theorem

mem_support_fromSpecStalk_of_stalkIdeal_le

L36 ↗
AlgebraicGeometry.Scheme.IdealSheafData.mem_support_fromSpecStalk_of_stalkIdeal_le
Documentation

A prime of 𝒪_{X,x} containing the stalk ideal represents a point of the support under the canonical morphism Spec 𝒪_{X,x} ⟶ X.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}}
Lean source · statement
theorem mem_support_fromSpecStalk_of_stalkIdeal_le
    (I : X.IdealSheafData) (x : X)
    (p : Spec (X.presheaf.stalk x))
    (hp : I.stalkIdeal x ≤ p.asIdeal) :
    X.fromSpecStalk x p ∈ I.support
theorem

map_stalkIdeal_stalkFromSpecStalkEquivLocalization

L72 ↗
AlgebraicGeometry.Scheme.IdealSheafData.map_stalkIdeal_stalkFromSpecStalkEquivLocalization
Documentation

Under the canonical identification of the stalk at a point of Spec 𝒪_{X,x} with a prime localization, the divisor stalk ideal is exactly the extension of the stalk ideal at x.

Source context 5 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}}
Lean source · statement
theorem map_stalkIdeal_stalkFromSpecStalkEquivLocalization
    (I : X.IdealSheafData) (x : X)
    (p : Spec (X.presheaf.stalk x)) :
    (I.stalkIdeal (X.fromSpecStalk x p)).map
        (X.stalkFromSpecStalkEquivLocalization x p).toRingHom =
      (I.stalkIdeal x).map
        (algebraMap (X.presheaf.stalk x)
          (@Localization.AtPrime (X.presheaf.stalk x) _
             (p : PrimeSpectrum (X.presheaf.stalk x)).asIdeal
             (PrimeSpectrum.isPrime (p : PrimeSpectrum (X.presheaf.stalk x)))))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.