Module

Local.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.DimensionTwo.IntegralClosure.Local

1 declaration indexed from sourceView source ↗

Module documentation

Purity for a normalization over a two-dimensional regular local ring

The full root cover used in the height-two Abhyankar argument, after the selected divisor root has also been adjoined, is a regular local ring of dimension two; it is not presented as a prime localization of a larger regular ring. This file supplies the corresponding intrinsic local-purity endpoint. The preceding conditional cover only classifies contractions of height-one primes; purity is applied to the full cover. Finiteness, freeness, and a regular parameter pair are constructed from the local base, so the only geometric input is etaleness at every height-one localization.

Imports1

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.DimensionTwo.IntegralClosure.HeightTwo

Imported by6

theorem

integralClosure_etale_of_isRegularLocalRing_dimension_two

L38 ↗

EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_etale_of_isRegularLocalRing_dimension_two

Documentation

A normalization in a finite separable extension of the fraction field of an arbitrary two-dimensional regular local domain is etale once all of its height-one localizations are etale. In the height-two Abhyankar consumer, the local domain is the full selected-root cover, not the preceding conditional cover.

The normalization is proved finite and free internally, and the required regular parameter pair is lifted from the cotangent space.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
open IsLocalRing
universe u v w

Lean source · statement

theorem integralClosure_etale_of_isRegularLocalRing_dimension_two
    {A : Type u} {K : Type v} {L : Type w}
    [CommRing A] [IsDomain A] [IsRegularLocalRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (hdim : ringKrullDim A = ((2 : ℕ∞) : WithBot ℕ∞))
    (hlocal : ∀ (q : Ideal A) [q.IsPrime], q.height = 1 →
      Algebra.Etale (Localization.AtPrime q)
        (Localization (Algebra.algebraMapSubmonoid
          (integralClosure A L) q.primeCompl))) :
    Algebra.Etale A (integralClosure A L)

Module documentation

Purity for a normalization over a two-dimensional regular local ring

Declarations

integralClosure_etale_of_isRegularLocalRing_dimension_two