Module

RegularLocalDimensionOne.lean

Nyll.SchemeTheory.RingTheory.RegularLocalDimensionOne

1 declaration indexed from sourceView source ↗

Module documentation

One-dimensional regular local rings are DVRs

Regularity supplies the domain structure and identifies the dimension of the cotangent space with Krull dimension. The one-dimensional local-domain criterion then produces the discrete valuation ring structure. No domain or normality hypothesis is added to regularity.

Imports6

Nyll.SchemeTheory.RingTheory.RegularLocalDomain
Mathlib.Data.ENat.Basic
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.KrullDimension.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Mathlib.RingTheory.RegularLocalRing.Defs

Imported by6

theorem

isDiscreteValuationRing_of_isRegularLocalRing_dimension_one

L29 ↗

SchemeTheory.isDiscreteValuationRing_of_isRegularLocalRing_dimension_one

Documentation

A regular local ring of dimension one is a DVR, with its domain structure derived from regularity and retained in the conclusion.

Source context 2 commands

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

namespace SchemeTheory
universe u

Lean source · full declaration

theorem isDiscreteValuationRing_of_isRegularLocalRing_dimension_one
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (hdim : ringKrullDim R = (1 : WithBot ℕ∞)) :
    let : IsDomain R := IsRegularLocalRing.isDomain R
    IsDiscreteValuationRing R := by
  intro hdomain
  apply IsLocalRing.finrank_CotangentSpace_eq_one_iff.mp
  have hcotangent :
      ((Module.finrank (IsLocalRing.ResidueField R)
        (IsLocalRing.CotangentSpace R) : ℕ∞) : WithBot ℕ∞) =
      ((1 : ℕ∞) : WithBot ℕ∞) :=
    ((IsRegularLocalRing.iff_finrank_cotangentSpace R).mp inferInstance).trans hdim
  exact ENat.natCast_inj.mp (WithBot.coe_eq_coe.mp hcotangent)

Module documentation

One-dimensional regular local rings are DVRs

Declarations

isDiscreteValuationRing_of_isRegularLocalRing_dimension_one