NYLL
Module

NormalizationPrime.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.NormalizationPrime
2 declarations indexed from sourceView source ↗

Module documentation

Strict Henselianity of an actual normalization prime localization

The integral closure in an algebraic separably closed extension has that extension as its fraction field, by the native algebraic integral-closure owner. Its literal prime localization is normal and has the same fraction field through the existing prescribed localization map. The established separably closed fraction-field theorem therefore proves strict Henselianity. No finite extension, Noetherianity, or separately chosen local model is used.

Imports5
Imported by6

Declarations

theorem

primeLocalization_strictHenselian

L31 ↗
EtaleFundamentalGroups.StrictHenselian.primeLocalization_strictHenselian
Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
universe u v w
Lean source · statement
theorem primeLocalization_strictHenselian
    (B : Type u) (L : Type v) [CommRing B] [IsDomain B] [IsIntegrallyClosed B]
    [Field L] [Algebra B L] [IsFractionRing B L] [IsSepClosed L]
    (Q : Ideal B) [Q.IsPrime] :
    HenselianLocalRing (Localization.AtPrime Q) ∧
      IsSepClosed (IsLocalRing.ResidueField (Localization.AtPrime Q))
theorem

integralClosure_localizationAtPrime_strictHenselian

L51 ↗
EtaleFundamentalGroups.StrictHenselian.integralClosure_localizationAtPrime_strictHenselian
Documentation

The literal localization of the integral closure at any prime is strictly Henselian when the ambient algebraic extension is separably closed. The base need only be a domain with the displayed fraction field; its normality and localness are not needed for this supplier.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.StrictHenselian
universe u v w
Lean source · statement
theorem integralClosure_localizationAtPrime_strictHenselian
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [Algebra.IsAlgebraic K L] [IsSepClosed L]
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] :
    HenselianLocalRing (Localization.AtPrime Q) ∧
      IsSepClosed (IsLocalRing.ResidueField (Localization.AtPrime Q))

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