Nyll.EtaleFundamentalGroups.Purity.RegularBoundaryStalkNormalization

Module documentation

Normalization over a regular boundary stalk

Regularity along the original boundary supplies regularity at precisely the boundary primes of the spectrum of a stalk. The canonical stalk-localization isomorphism makes this transfer without assuming regularity of the entire scheme or of every localization of an arbitrary regular local ring.

theorem

integralClosure_stalk_etale_of_regular_boundary

L34 ↗

EtaleFundamentalGroups.integralClosure_stalk_etale_of_regular_boundary

Documentation

Over the stalk of any regular boundary point, a finite separable normalization that is étale off the boundary and at height-one primes is étale everywhere. All domain and normality hypotheses on the stalk are produced from the original boundary regularity assumption.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem integralClosure_stalk_etale_of_regular_boundary
    {X : Scheme.{u}} (I : X.IdealSheafData)
    (hregular : I.IsAmbientRegularAlongSupport)
    (x : X) (hx : x ∈ I.support)
    {K L : Type u} [Field K] [Algebra (X.presheaf.stalk x) K]
    [IsFractionRing (X.presheaf.stalk x) K]
    [Field L] [Algebra (X.presheaf.stalk x) L] [Algebra K L]
    [IsScalarTower (X.presheaf.stalk x) K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (haway : ∀ P : PrimeSpectrum (integralClosure (X.presheaf.stalk x) L),
      X.fromSpecStalk x
          (PrimeSpectrum.comap
            (algebraMap (X.presheaf.stalk x) (integralClosure (X.presheaf.stalk x) L)) P)
          ∉ I.support →
        Algebra.IsEtaleAt (X.presheaf.stalk x) P.asIdeal)
    (hheightOne : ∀ (p : Ideal (X.presheaf.stalk x)) [p.IsPrime], p.height = 1 →
      ∀ (P : Ideal (integralClosure (X.presheaf.stalk x) L)) [P.IsPrime] [P.LiesOver p],
        Algebra.IsEtaleAt (X.presheaf.stalk x) P) :
    Algebra.Etale (X.presheaf.stalk x) (integralClosure (X.presheaf.stalk x) L)

Module documentation

Normalization over a regular boundary stalk

Declarations

integralClosure_stalk_etale_of_regular_boundary