Nyll.SchemeTheory.RingTheory.Descent.FiniteNormalizationModel

Module documentation

A finite model of a normalization near one base prime

The model is a genuine subalgebra of the original algebra on D(d). It recovers that algebra after inverting d, and agrees with the integral closure at the selected prime. Its generators come from the two actual localizations, rather than from a finiteness assumption on the normalization.

theorem

exists_finite_normalization_model

L33 ↗

SchemeTheory.exists_finite_normalization_model

Documentation

Finite generation of the normalization at one prime and on D(d) produces a finite model inside the original algebra, with both comparisons.

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_normalization_model
    {R : Type u} [CommRing 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)] :
    ∃ C : Subalgebra R T, Module.Finite R C ∧
      IsLocalization.Away (algebraMap R C d) T ∧
      Nonempty ((Localization.AtPrime p.asIdeal ⊗[R] C) ≃ₐ[Localization.AtPrime p.asIdeal]
        (Localization.AtPrime p.asIdeal ⊗[R] integralClosure R T))

Module documentation

A finite model of a normalization near one base prime

Declarations

exists_finite_normalization_model