Module

FiniteNormalizationLocalCriterion.lean

Nyll.EtaleFundamentalGroups.Normalization.FiniteNormalizationLocalCriterion

3 declarations indexed from sourceView source ↗

Module documentation

Non-Noetherian spreading for finite field normalizations

A finite subalgebra with the correct fraction field becomes the actual normalization on each neighborhood where it is étale. Local finiteness and étaleness at a base prime therefore spread without any Noetherian hypothesis.

Imports7

Nyll.EtaleFundamentalGroups.Normalization.FiniteFractionFieldModel
Nyll.EtaleFundamentalGroups.Normalization.FiniteNormalModelNeighborhood
Nyll.SchemeTheory.RingTheory.Descent.EtaleAtPrimeNormality
Mathlib.Algebra.Algebra.Subalgebra.Tower
Mathlib.RingTheory.LocalProperties.IntegrallyClosed
Mathlib.RingTheory.Localization.AsSubring
Mathlib.RingTheory.Smooth.IntegralClosure

Imported by3

theorem

finite_etale_integralClosure_of_finite_model_away

L35 ↗

EtaleFundamentalGroups.finite_etale_integralClosure_of_finite_model_away

Documentation

An étale neighborhood of a finite subalgebra with the original fraction field is the actual finite étale normalization on that neighborhood.

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_integralClosure_of_finite_model_away
    {R L : Type u} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [Field L] [Algebra R L]
    (C : Subalgebra R L) [Module.Finite R C] [IsFractionRing C L]
    (r : R) (hr : r ≠ 0) [FaithfulSMul R L]
    [Algebra.Etale R (Localization.Away (algebraMap R C r))] :
    Module.Finite (Localization.Away r)
        (Localization.Away r ⊗[R] integralClosure R L) ∧
      Algebra.Etale (Localization.Away r)
        (Localization.Away r ⊗[R] integralClosure R L)

theorem

exists_finite_etale_normalization_away_of_localized_etale

L103 ↗

EtaleFundamentalGroups.exists_finite_etale_normalization_away_of_localized_etale

Documentation

A finite étale localization of the actual normalization at one base prime spreads to a principal neighborhood for any normal domain.

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 exists_finite_etale_normalization_away_of_localized_etale
    (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] (p : PrimeSpectrum R)
    [Module.Finite (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R L)]
    [Algebra.Etale (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R L)] :
    ∃ r : R, r ∉ p.asIdeal ∧
      Module.Finite (Localization.Away r)
        (Localization.Away r ⊗[R] integralClosure R L) ∧
      Algebra.Etale (Localization.Away r)
        (Localization.Away r ⊗[R] integralClosure R L)

theorem

finite_etale_normalization_of_localized_finite_etale

L143 ↗

EtaleFundamentalGroups.finite_etale_normalization_of_localized_finite_etale

Documentation

Finite étaleness of all actual base-prime localizations implies finite étaleness of the normalization itself, for arbitrary normal domains.

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_finite_etale
    (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,
      Module.Finite (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R L) ∧
        Algebra.Etale (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

Non-Noetherian spreading for finite field normalizations

Declarations

finite_etale_integralClosure_of_finite_model_away

exists_finite_etale_normalization_away_of_localized_etale

finite_etale_normalization_of_localized_finite_etale