Module

DimensionOneRegularRing.lean

Nyll.SchemeTheory.LocalGeometry.RegularLocal.DimensionOneRegularRing

1 declaration indexed from sourceView source ↗

Module documentation

One-dimensional regular local domains are regular rings

In dimension one every nonzero prime of a local domain is maximal. Thus a one-dimensional regular local domain is regular at all of its primes without using the missing general theorem that arbitrary regular local rings are regular rings.

Imports1

Mathlib.RingTheory.RegularLocalRing.Defs

Imported by2

theorem

isRegularRing_of_isRegularLocalRing_dimension_one

L27 ↗

EtaleFundamentalGroups.isRegularRing_of_isRegularLocalRing_dimension_one

Documentation

A one-dimensional regular local domain is a regular 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 isRegularRing_of_isRegularLocalRing_dimension_one
    {R : Type u} [CommRing R] [IsDomain R] [IsRegularLocalRing R]
    (hdim : ringKrullDim R = ((1 : ℕ∞) : WithBot ℕ∞)) :
    IsRegularRing R

Module documentation

One-dimensional regular local domains are regular rings

Declarations

isRegularRing_of_isRegularLocalRing_dimension_one