Module

RegularLocalDimensionTwoDVR.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.HeightOne.RegularLocalDimensionTwoDVR

1 declaration indexed from sourceView source ↗

Module documentation

Height-one localizations of two-dimensional regular local domains

A two-dimensional regular local domain is integrally closed. Localizing at a height-one prime preserves integral closedness and Noetherianity, and the localized ring has Krull dimension one. Thus it is a non-field normal Noetherian local domain with a unique nonzero prime, hence a discrete valuation ring.

This argument deliberately does not pass through an IsRegularRing instance on the original local ring.

Imports2

Mathlib.RingTheory.DiscreteValuationRing.TFAE
Nyll.EtaleFundamentalGroups.LocalGeometry.RegularLocal.DimensionTwoIntegrallyClosed

Imported by5

theorem

isDiscreteValuationRing_localizationAtPrime_of_isRegularLocalRing_dimension_two

L33 ↗

EtaleFundamentalGroups.isDiscreteValuationRing_localizationAtPrime_of_isRegularLocalRing_dimension_two

Documentation

The localization of a two-dimensional regular local domain at a height-one prime is a discrete valuation ring.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
universe u

Lean source · statement

theorem isDiscreteValuationRing_localizationAtPrime_of_isRegularLocalRing_dimension_two
    {D : Type u} [CommRing D] [IsDomain D] [IsRegularLocalRing D]
    (hdim : ringKrullDim D = ((2 : ℕ∞) : WithBot ℕ∞))
    (q : Ideal D) [q.IsPrime] (hqHeight : q.height = 1) :
    IsDiscreteValuationRing (Localization.AtPrime q)

Module documentation

Height-one localizations of two-dimensional regular local domains

Declarations

isDiscreteValuationRing_localizationAtPrime_of_isRegularLocalRing_dimension_two