Nyll.SchemeTheory.RingTheory.Descent.FiniteNormalizationNeighborhood

Module documentation

Identifying a normalization on an etale neighborhood of a finite model

A finite model becomes etale after shrinking the base. Normality of the original base along the boundary then makes the model's boundary local rings normal. Integral closure across that boundary identifies the model with the actual relative normalization, proving both finiteness and etaleness there.

theorem

finite_etale_integralClosure_on_model_neighborhood

L34 ↗

SchemeTheory.finite_etale_integralClosure_on_model_neighborhood

Documentation

An etale neighborhood of a finite model is an etale neighborhood of the actual normalization, provided the 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 nonZeroDivisors
universe u
attribute [local instance] Algebra.TensorProduct.rightAlgebra

Lean source · statement

theorem finite_etale_integralClosure_on_model_neighborhood
    {R T : Type u} [CommRing R] [CommRing T] [Algebra R T]
    (C : Subalgebra R T) [Module.Finite R C]
    (d r : R) [IsLocalization.Away (algebraMap R C d) T]
    [Algebra.Etale R (Localization.Away (algebraMap R C r))]
    (hnormal : ∀ (p : Ideal R) [p.IsPrime], d ∈ p →
      IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)) :
    Module.Finite (Localization.Away r)
        (Localization.Away r ⊗[R] integralClosure R T) ∧
      Algebra.Etale (Localization.Away r)
        (Localization.Away r ⊗[R] integralClosure R T)

Module documentation

Identifying a normalization on an etale neighborhood of a finite model

Declarations

finite_etale_integralClosure_on_model_neighborhood