NYLL
Module

RegularBoundaryPurity.lean

Nyll.EtaleFundamentalGroups.Purity.SpecialLocal.RegularBoundaryPurity
2 declarations indexed from sourceView source ↗

Module documentation

Purity along a regular boundary

A hypothetical minimal non-étale point belongs to the specified boundary, because the algebra is étale off that boundary. Generic and height-one étaleness force its height to be at least two. Its regular local ring then has punctured purity, contradicting the minimal non-étale point criterion. Regularity is required only on the boundary, not on the whole base.

Imports8
Imported by3

Declarations

theorem

finiteNormalDomainAlgebra_etale_of_regular_boundary

L34 ↗
EtaleFundamentalGroups.SpecialLocalPurity.finiteNormalDomainAlgebra_etale_of_regular_boundary
Documentation

A finite normal-domain algebra is étale if it is generically étale, étale in codimension one, and étale outside a boundary of regular points.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u
Lean source · statement
theorem finiteNormalDomainAlgebra_etale_of_regular_boundary
    {R S : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsNoetherianRing R] [CommRing S] [IsDomain S] [IsIntegrallyClosed S]
    [Algebra R S] [Module.Finite R S]
    (hinj : Function.Injective (algebraMap R S))
    (Z : Set (PrimeSpectrum R))
    (hregular : ∀ p ∈ Z, IsRegularLocalRing (Localization.AtPrime p.asIdeal))
    (hgeneric : Algebra.IsEtaleAt R (⊥ : Ideal S))
    (haway : ∀ P : PrimeSpectrum S,
      PrimeSpectrum.comap (algebraMap R S) P ∉ Z → Algebra.IsEtaleAt R P.asIdeal)
    (hheightOne : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 →
      ∀ (P : Ideal S) [P.IsPrime] [P.LiesOver p], Algebra.IsEtaleAt R P) :
    Algebra.Etale R S
theorem

integralClosure_etale_of_regular_boundary

L87 ↗
EtaleFundamentalGroups.SpecialLocalPurity.integralClosure_etale_of_regular_boundary
Documentation

The normalization in a finite separable function-field extension is étale when the branch locus is confined to regular boundary points and no height-one ramification remains. Finiteness and generic étaleness of the actual integral closure are supplied internally.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.SpecialLocalPurity
universe u
Lean source · statement
theorem integralClosure_etale_of_regular_boundary
    {R K L : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [IsNoetherianRing R] [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (Z : Set (PrimeSpectrum R))
    (hregular : ∀ p ∈ Z, IsRegularLocalRing (Localization.AtPrime p.asIdeal))
    (haway : ∀ P : PrimeSpectrum (integralClosure R L),
      PrimeSpectrum.comap (algebraMap R (integralClosure R L)) P ∉ Z →
        Algebra.IsEtaleAt R P.asIdeal)
    (hheightOne : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 →
      ∀ (P : Ideal (integralClosure R L)) [P.IsPrime] [P.LiesOver p],
        Algebra.IsEtaleAt R P) :
    Algebra.Etale R (integralClosure R L)

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