NYLL
Module

PuncturedSpectrumCover.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumCover
14 declarations indexed from sourceView source ↗

Module documentation

A finite affine cover of a punctured local spectrum

For a Noetherian local ring, the maximal ideal has a finite generating set. The corresponding principal opens cover the complement of the closed point. This file constructs that cover on the actual punctured spectrum, proves its charts affine, and identifies every chart with the spectrum of the canonical away localization.

Imports4
Imported by3

Declarations

abbrev

puncturedSpectrumGeneratorIndex

L34 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumGeneratorIndex
Documentation

The finite index type of the chosen minimal-cardinality generating set of the maximal ideal.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
abbrev puncturedSpectrumGeneratorIndex
instance

puncturedSpectrumGeneratorIndex_finite

L37 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumGeneratorIndex_finite
Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
instance puncturedSpectrumGeneratorIndex_finite :
    Finite (puncturedSpectrumGeneratorIndex R)
def

puncturedSpectrumGenerator

L46 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumGenerator
Documentation

A generator of the maximal ideal indexing a principal chart of the punctured spectrum.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumGenerator
    (i : puncturedSpectrumGeneratorIndex R) : R
theorem

puncturedSpectrumGenerator_mem_maximalIdeal

L51 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumGenerator_mem_maximalIdeal
Source context 6 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumGenerator_mem_maximalIdeal
    (i : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumGenerator R i ∈ maximalIdeal R
def

puncturedSpectrumAmbientBasicOpen

L58 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientBasicOpen
Documentation

The ambient principal open associated to one chosen maximal-ideal generator.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumAmbientBasicOpen
    (i : puncturedSpectrumGeneratorIndex R) :
    (Spec (.of R)).Opens
theorem

puncturedSpectrumAmbientBasicOpen_le

L66 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAmbientBasicOpen_le
Source context 6 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumAmbientBasicOpen_le
    (i : puncturedSpectrumGeneratorIndex R) :
    puncturedSpectrumAmbientBasicOpen R i ≤ puncturedSpectrumOpen R
theorem

iSup_puncturedSpectrumAmbientBasicOpen

L79 ↗
AlgebraicGeometry.Scheme.iSup_puncturedSpectrumAmbientBasicOpen
Source context 6 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem iSup_puncturedSpectrumAmbientBasicOpen :
    (⨆ i : puncturedSpectrumGeneratorIndex R,
      puncturedSpectrumAmbientBasicOpen R i) =
        puncturedSpectrumOpen R
def

puncturedSpectrumBasicOpen

L109 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumBasicOpen
Documentation

One principal chart, now regarded as an open of the punctured spectrum.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumBasicOpen
    (i : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrum R).Opens
theorem

puncturedSpectrumBasicOpen_isOpenCover

L117 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumBasicOpen_isOpenCover
Source context 6 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumBasicOpen_isOpenCover :
    IsOpenCover (puncturedSpectrumBasicOpen R)
def

puncturedSpectrumBasicOpenIsoSpecAway

L127 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumBasicOpenIsoSpecAway
Documentation

A principal chart of the punctured spectrum is canonically the spectrum of the localization obtained by inverting its indexing generator.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumBasicOpenIsoSpecAway
    (i : puncturedSpectrumGeneratorIndex R) :
    (puncturedSpectrumBasicOpen R i).toScheme ≅
      Spec (.of (Localization.Away (puncturedSpectrumGenerator R i)))
theorem

puncturedSpectrumBasicOpen_isAffine

L140 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumBasicOpen_isAffine
Source context 6 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
omit [IsNoetherianRing R] in
Lean source · statement
theorem puncturedSpectrumBasicOpen_isAffine
    (i : puncturedSpectrumGeneratorIndex R) :
    IsAffineOpen (puncturedSpectrumBasicOpen R i)
def

puncturedSpectrumOpenCover

L146 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumOpenCover
Documentation

The finite open cover whose members are the actual principal charts.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumOpenCover : (puncturedSpectrum R).OpenCover
def

puncturedSpectrumAffineOpenCover

L152 ↗
AlgebraicGeometry.Scheme.puncturedSpectrumAffineOpenCover
Documentation

The same finite cover packaged as an affine open cover.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
def puncturedSpectrumAffineOpenCover :
    (puncturedSpectrum R).AffineOpenCover
theorem

compactSpace_puncturedSpectrum

L161 ↗
AlgebraicGeometry.Scheme.compactSpace_puncturedSpectrum
Documentation

The punctured spectrum of a Noetherian local ring is quasi-compact. The proof uses the finite principal affine cover constructed above.

Source context 5 commands

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

noncomputable section
open IsLocalRing TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem compactSpace_puncturedSpectrum : CompactSpace (puncturedSpectrum R)

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