Module

PuncturedDVR.lean

Nyll.SchemeTheory.LocalGeometry.PuncturedDVR

5 declarations indexed from sourceView source ↗

Module documentation

The punctured spectrum of a discrete valuation ring

The fraction field of a DVR is its localization away from any uniformizer. Consequently its spectrum is the actual open complement of the closed point. The resulting scheme isomorphism retains the canonical map to the full spectrum, so covers of the puncture and of the fraction field can be compared without replacing their structure maps.

Imports11

Nyll.SchemeTheory.LocalGeometry.PuncturedSpectrum
Nyll.SchemeTheory.RingTheory.DVRFractionFieldAway
Mathlib.Algebra.GroupWithZero.Associated
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Restrict
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.Ideal.Span
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Localization.Basic
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by3

theorem

puncturedSpectrumOpen_eq_basicOpen_of_uniformizer

L38 ↗

AlgebraicGeometry.Scheme.puncturedSpectrumOpen_eq_basicOpen_of_uniformizer

Documentation

The puncture of a DVR is the principal open of any uniformizer.

Source context 4 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u

Lean source · statement

theorem puncturedSpectrumOpen_eq_basicOpen_of_uniformizer
    (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    {π : R} (hπ : Irreducible π) :
    puncturedSpectrumOpen R = PrimeSpectrum.basicOpen π

theorem

isOpenImmersion_SpecMap_fractionField_of_dvr

L61 ↗

AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_fractionField_of_dvr

Documentation

The canonical map from a DVR's fraction-field spectrum is an open immersion. Its localization presentation is derived from the DVR.

Source context 4 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u

Lean source · statement

theorem isOpenImmersion_SpecMap_fractionField_of_dvr
    (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field K] [Algebra R K] [IsFractionRing R K] :
    IsOpenImmersion (Spec.map (CommRingCat.ofHom (algebraMap R K)))

theorem

range_SpecMap_fractionField_of_dvr

L73 ↗

AlgebraicGeometry.Scheme.range_SpecMap_fractionField_of_dvr

Documentation

The canonical fraction-field spectrum has exactly the puncture as its image, with the original R-algebra structure on the fraction field.

Source context 4 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u

Lean source · statement

theorem range_SpecMap_fractionField_of_dvr
    (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field K] [Algebra R K] [IsFractionRing R K] :
    Set.range (Spec.map (CommRingCat.ofHom (algebraMap R K))) =
      (puncturedSpectrumOpen R : Set (Spec (.of R)))

def

puncturedSpectrumIsoSpecFractionField

L89 ↗

AlgebraicGeometry.Scheme.puncturedSpectrumIsoSpecFractionField

Documentation

The puncture of a DVR is its fraction-field spectrum, as schemes over that DVR.

Source context 4 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u

Lean source · statement

def puncturedSpectrumIsoSpecFractionField
    (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field K] [Algebra R K] [IsFractionRing R K] :
    puncturedSpectrum R ≅ Spec (.of K)

theorem

puncturedSpectrumIsoSpecFractionField_hom_SpecMap

L102 ↗

AlgebraicGeometry.Scheme.puncturedSpectrumIsoSpecFractionField_hom_SpecMap

Documentation

The puncture/fraction-field comparison preserves the map to Spec R.

Source context 4 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u

Lean source · statement

theorem puncturedSpectrumIsoSpecFractionField_hom_SpecMap
    (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    [Field K] [Algebra R K] [IsFractionRing R K] :
    (puncturedSpectrumIsoSpecFractionField R K).hom ≫
        Spec.map (CommRingCat.ofHom (algebraMap R K)) =
      puncturedSpectrumInclusion R

Module documentation

The punctured spectrum of a discrete valuation ring

Declarations

puncturedSpectrumOpen_eq_basicOpen_of_uniformizer

isOpenImmersion_SpecMap_fractionField_of_dvr

range_SpecMap_fractionField_of_dvr

puncturedSpectrumIsoSpecFractionField

puncturedSpectrumIsoSpecFractionField_hom_SpecMap