Module

NormalLocalizationDVR.lean

Nyll.SchemeTheory.LocalGeometry.HeightOne.NormalLocalizationDVR

1 declaration indexed from sourceView source ↗

Module documentation

Height-one localizations of Noetherian normal domains

A height-one localization of a Noetherian integrally closed domain is a one-dimensional normal Noetherian local domain, hence a DVR. This is the form needed for height-one primes in finite normalizations; no regularity of the unlocalized normalization is required.

Imports4

Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.DedekindDomain.Dvr
Mathlib.RingTheory.Ideal.Height
Mathlib.RingTheory.Localization.Submodule

Imported by4

theorem

isDiscreteValuationRing_localizationAtPrime_of_normal_noetherian_height_one

L30 ↗

EtaleFundamentalGroups.isDiscreteValuationRing_localizationAtPrime_of_normal_noetherian_height_one

Documentation

A height-one localization of a Noetherian normal domain is a DVR.

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_normal_noetherian_height_one
    {S : Type u} [CommRing S] [IsDomain S] [IsNoetherianRing S]
    [IsIntegrallyClosed S]
    (q : Ideal S) [q.IsPrime] (hqHeight : q.height = 1) :
    IsDiscreteValuationRing (Localization.AtPrime q)

Module documentation

Height-one localizations of Noetherian normal domains

Declarations

isDiscreteValuationRing_localizationAtPrime_of_normal_noetherian_height_one