Module

PuncturedSpectrum.lean

Nyll.SchemeTheory.LocalGeometry.PuncturedSpectrum

5 declarations indexed from sourceView source ↗

Module documentation

The punctured spectrum of a local ring

This module supplies the canonical open complement of the closed point and its basic nonemptiness criterion.

Imports2

Mathlib.RingTheory.Ideal.Height
Nyll.SchemeTheory.Normalization.Normal

Imported by18

def

puncturedSpectrumOpen

L28 ↗

AlgebraicGeometry.Scheme.puncturedSpectrumOpen

Documentation

The complement of the closed point in the spectrum of a local ring.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace Scheme

Lean source · statement

def puncturedSpectrumOpen (R : Type u) [CommRing R] [IsLocalRing R] :
    (Spec (.of R)).Opens

abbrev

puncturedSpectrum

L33 ↗

AlgebraicGeometry.Scheme.puncturedSpectrum

Documentation

The punctured spectrum of a local ring.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace Scheme

Lean source · statement

abbrev puncturedSpectrum (R : Type u) [CommRing R] [IsLocalRing R] :
    Scheme.{u}

def

puncturedSpectrumInclusion

L39 ↗

AlgebraicGeometry.Scheme.puncturedSpectrumInclusion

Documentation

The canonical open immersion from the punctured spectrum into the full local spectrum.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace Scheme

Lean source · statement

def puncturedSpectrumInclusion (R : Type u) [CommRing R] [IsLocalRing R] :
    puncturedSpectrum R ⟶ Spec (.of R)

theorem

mem_puncturedSpectrumOpen_iff

L44 ↗

AlgebraicGeometry.Scheme.mem_puncturedSpectrumOpen_iff

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace Scheme

Lean source · statement

theorem mem_puncturedSpectrumOpen_iff
    (R : Type u) [CommRing R] [IsLocalRing R]
    (x : PrimeSpectrum R) :
    x ∈ puncturedSpectrumOpen R ↔ x ≠ closedPoint R

theorem

puncturedSpectrum_nonempty_of_one_le_ringKrullDim

L54 ↗

AlgebraicGeometry.Scheme.puncturedSpectrum_nonempty_of_one_le_ringKrullDim

Documentation

A positive-dimensional local domain has a nonempty punctured spectrum: its generic point is different from the closed point.

Source context 5 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry
universe u
namespace Scheme

Lean source · statement

theorem puncturedSpectrum_nonempty_of_one_le_ringKrullDim
    (R : Type u) [CommRing R] [IsDomain R] [IsLocalRing R]
    (hdim : (1 : WithBot ℕ∞) ≤ ringKrullDim R) :
    Nonempty (puncturedSpectrum R)

Module documentation

The punctured spectrum of a local ring

Declarations

puncturedSpectrumOpen

puncturedSpectrum

puncturedSpectrumInclusion

mem_puncturedSpectrumOpen_iff

puncturedSpectrum_nonempty_of_one_le_ringKrullDim