Module

DimensionTwoIntegrallyClosed.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.RegularLocal.DimensionTwoIntegrallyClosed

2 declarations indexed from sourceView source ↗

Module documentation

Normality of two-dimensional regular local domains

Mathlib's current definition of a regular ring directly asks for regularity of every prime localization; it does not yet provide the converse theorem that a regular local ring is regular. In dimension two, the explicit regular-pair construction supplies the normality statement needed by the generic-component normalization argument without that missing general localization theorem.

Imports2

Imported by11

theorem

isIntegrallyClosed_of_isRegularLocalRing_dimension_two

L33 ↗

EtaleFundamentalGroups.SpecialLocalPurity.isIntegrallyClosed_of_isRegularLocalRing_dimension_two

Documentation

A two-dimensional regular local domain is integrally closed.

The regular pair is produced from a basis of the cotangent space and is not part of the theorem's input.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
universe u

Lean source · statement

theorem isIntegrallyClosed_of_isRegularLocalRing_dimension_two
    {A : Type u} [CommRing A] [IsDomain A] [IsRegularLocalRing A]
    (hdim : ringKrullDim A = ((2 : ℕ∞) : WithBot ℕ∞)) :
    IsIntegrallyClosed A

theorem

isIntegrallyClosed_localizationAtPrime_of_height_eq_two

L51 ↗

EtaleFundamentalGroups.SpecialLocalPurity.isIntegrallyClosed_localizationAtPrime_of_height_eq_two