NYLL
Module

FiniteNormalizationSpreading.lean

Nyll.SchemeTheory.RingTheory.Descent.FiniteNormalizationSpreading
3 declarations indexed from sourceView source ↗

Module documentation

Spreading finite etale normalizations from base local rings

Finiteness at a point first produces an actual finite subalgebra model. Its etale locus spreads around the whole fiber, and boundary normality identifies that model with the integral closure on this neighborhood. The resulting principal neighborhoods then give global finite generation.

Imports7
Imported by2

Declarations

theorem

exists_finite_etale_integralClosure_away

L36 ↗
SchemeTheory.exists_finite_etale_integralClosure_away
Documentation

A finite etale normalization at one base prime spreads to a principal neighborhood when the original base is normal along the boundary.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u
attribute [local instance] Algebra.TensorProduct.rightAlgebra
Lean source · statement
theorem exists_finite_etale_integralClosure_away
    {R : Type u} [CommRing R] [IsNoetherianRing R] (d : R)
    (A : Type u) [CommRing A] [Algebra R A] [IsLocalization.Away d A]
    (T : Type u) [CommRing T] [Algebra R T] [Algebra A T]
    [IsScalarTower R A T] [Module.Finite A T]
    (p : PrimeSpectrum R)
    [Module.Finite (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R T)]
    [Algebra.Etale (Localization.AtPrime p.asIdeal)
      (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R T)]
    (hnormal : ∀ (q : Ideal R) [q.IsPrime], d ∈ q →
      IsDomain (Localization.AtPrime q) ∧ IsIntegrallyClosed (Localization.AtPrime q)) :
    ∃ r : R, r ∉ p.asIdeal ∧
      Module.Finite (Localization.Away r)
        (Localization.Away r ⊗[R] integralClosure R T) ∧
      Algebra.Etale (Localization.Away r)
        (Localization.Away r ⊗[R] integralClosure R T)
theorem

finite_of_finite_tensor_neighborhoods

L68 ↗
SchemeTheory.finite_of_finite_tensor_neighborhoods
Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u
attribute [local instance] Algebra.TensorProduct.rightAlgebra
Lean source · statement
theorem finite_of_finite_tensor_neighborhoods
    {R B : Type u} [CommRing R] [CommRing B] [Algebra R B]
    (h : ∀ p : PrimeSpectrum R, ∃ r : R, r ∉ p.asIdeal ∧
      Module.Finite (Localization.Away r) (Localization.Away r ⊗[R] B)) :
    Module.Finite R B
theorem

finite_etale_integralClosure_of_local_finite_etale

L89 ↗
SchemeTheory.finite_etale_integralClosure_of_local_finite_etale
Documentation

Pointwise finite etale normalizations over the base local rings glue to the actual finite etale integral closure. Normality is used only on V(d). In particular no global normality of the original base is required.

Source context 5 commands

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

noncomputable section
namespace SchemeTheory
open scoped TensorProduct
universe u
attribute [local instance] Algebra.TensorProduct.rightAlgebra
Lean source · statement
theorem finite_etale_integralClosure_of_local_finite_etale
    {R : Type u} [CommRing R] [IsNoetherianRing R] (d : R)
    (A : Type u) [CommRing A] [Algebra R A] [IsLocalization.Away d A]
    (T : Type u) [CommRing T] [Algebra R T] [Algebra A T]
    [IsScalarTower R A T] [Module.Finite A T]
    (hnormal : ∀ (p : Ideal R) [p.IsPrime], d ∈ p →
      IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p))
    (hlocal : ∀ p : PrimeSpectrum R,
      Module.Finite (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R T) ∧
        Algebra.Etale (Localization.AtPrime p.asIdeal)
          (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R T)) :
    Module.Finite R (integralClosure R T) ∧ Algebra.Etale R (integralClosure R T)

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