Module

PrincipalDVR.lean

Nyll.SchemeTheory.LocalGeometry.HeightOne.PrincipalDVR

1 declaration indexed from sourceView source ↗

Module documentation

A Noetherian-free DVR criterion in dimension one

A local domain of Krull dimension at most one whose nonzero maximal ideal is principal is a discrete valuation ring. The usual DVR TFAE in mathlib assumes Noetherianity. Here Noetherianity is a conclusion rather than an input: the unique nonzero-prime geometry forces every nonzero element to be a unit times a power of a generator of the maximal ideal.

This form is intended for local rings cut out inside an adic base change, where a global IsNoetherianRing instance on the completion is not available. A retained generic component supplies the dimension bound, and the exact vertical-fibre calculation supplies the principal maximal ideal.

Imports3

Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Mathlib.RingTheory.KrullDimension.Basic

Imported by2

theorem

isDiscreteValuationRing_of_krullDimLE_one_of_maximalIdeal_isPrincipal

L42 ↗

EtaleFundamentalGroups.isDiscreteValuationRing_of_krullDimLE_one_of_maximalIdeal_isPrincipal

Documentation

A one-dimensional local domain with nonzero principal maximal ideal is a DVR, without a Noetherian hypothesis.

The proof first obtains a prime generator varpi of the maximal ideal. Every minimal prime above (x) for x != 0 is a nonzero prime, hence the unique maximal ideal by KrullDimLE 1. Thus a power of varpi belongs to (x). Cancelling one varpi at a time gives the required unit-times-power factorization, from which mathlib constructs the local PID.

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_of_krullDimLE_one_of_maximalIdeal_isPrincipal
    {A : Type u} [CommRing A] [IsDomain A] [IsLocalRing A]
    [Ring.KrullDimLE 1 A]
    (hnotField : ¬ IsField A)
    (hprincipal : (IsLocalRing.maximalIdeal A).IsPrincipal) :
    IsDiscreteValuationRing A

Module documentation

A Noetherian-free DVR criterion in dimension one

Declarations

isDiscreteValuationRing_of_krullDimLE_one_of_maximalIdeal_isPrincipal