NYLL
Module

DimensionTwoRegularRing.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.RegularLocal.DimensionTwoRegularRing
1 declaration indexed from sourceView source ↗

Module documentation

Two-dimensional regular local domains are regular rings

Mathlib defines a regular ring through regularity at every prime and does not yet contain the general theorem that a regular local ring is a regular ring. In the two-dimensional domain case needed here, the missing localization statement follows directly from the prime-height trichotomy: the generic point is a field, every nonmaximal nonzero prime has height one and hence a DVR localization, and localization at the maximal ideal is the original regular local ring.

Imports2
Imported by4

Declarations

theorem

isRegularRing_of_isRegularLocalRing_dimension_two

L31 ↗
EtaleFundamentalGroups.isRegularRing_of_isRegularLocalRing_dimension_two
Documentation

A two-dimensional regular local domain is regular at every prime.

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 isRegularRing_of_isRegularLocalRing_dimension_two
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    (hdim : ringKrullDim R = ((2 : ℕ∞) : WithBot ℕ∞)) :
    IsRegularRing R

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.