Nyll.EtaleFundamentalGroups.Normalization.LocalUnramifiedCriterion

Module documentation

The original local unramified criterion for normalization algebras

For the integral closure of a normal domain in a finite fraction-field extension, unramifiedness after localization at every base prime implies finite étaleness globally. Domain and faithfulness of each localization are derived from the actual integral-closure inclusion and flat localization.

theorem

finite_etale_normalization_of_localized_unramified

L35 ↗

EtaleFundamentalGroups.finite_etale_normalization_of_localized_unramified

Documentation

The ring form of the original implication (5) ⇒ (2) in Tag 0BTF. Only unramifiedness of the actual localized integral closures is assumed.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct nonZeroDivisors
universe u
attribute [local instance] Algebra.TensorProduct.rightAlgebra

Lean source · statement

theorem finite_etale_normalization_of_localized_unramified
    (R K L : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field L] [Algebra R L] [Algebra K L] [IsScalarTower R K L]
    [FiniteDimensional K L]
    (hlocal : ∀ p : PrimeSpectrum R,
      Algebra.FiniteType (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R L) ∧
        Algebra.FormallyUnramified (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R L)) :
    Module.Finite R (integralClosure R L) ∧ Algebra.Etale R (integralClosure R L)

Module documentation

The original local unramified criterion for normalization algebras

Declarations

finite_etale_normalization_of_localized_unramified