NYLL
Module

IntegralClosureLocalizationAway.lean

Nyll.SchemeTheory.RingTheory.Descent.IntegralClosureLocalizationAway
2 declarations indexed from sourceView source ↗

Module documentation

Recovering an algebra from its relative integral closure

If T is integral over a localization of R, its integral closure over R recovers T after inverting the original denominators. This is an application of Mathlib's integral-closure localization theorem, transported along the literal bijective inclusion of the integral closure over the localized base. The existing principal-localization API is the powers-submonoid specialization.

Imports5
  • Mathlib.Algebra.Algebra.Subalgebra.Tower
  • Mathlib.RingTheory.IntegralClosure.Algebra.Basic
  • Mathlib.RingTheory.Localization.Basic
  • Mathlib.RingTheory.Localization.Away.Basic
  • Mathlib.RingTheory.Localization.Integral
Imported by4

Declarations

theorem

integralClosure_isLocalization

L33 ↗
SchemeTheory.integralClosure_isLocalization
Documentation

Recover an integral algebra over a localization from its actual relative integral closure. The localization theorem and its transport are the existing Mathlib constructions; the only extra comparison is the literal inclusion.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
theorem integralClosure_isLocalization
    {R : Type u} [CommRing R] (M : Submonoid R)
    (A : Type v) [CommRing A] [Algebra R A] [IsLocalization M A]
    (T : Type w) [CommRing T] [Algebra R T] [Algebra A T]
    [IsScalarTower R A T] [Algebra.IsIntegral A T] :
    IsLocalization (Algebra.algebraMapSubmonoid (integralClosure R T) M) T
theorem

integralClosure_isLocalization_away

L64 ↗
SchemeTheory.integralClosure_isLocalization_away
Documentation

The relative integral closure in an integral R[1/d]-algebra has that original algebra as its principal localization.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v w
Lean source · statement
theorem integralClosure_isLocalization_away
    {R : Type u} [CommRing R] (d : R)
    (A : Type v) [CommRing A] [Algebra R A] [IsLocalization.Away d A]
    (T : Type w) [CommRing T] [Algebra R T] [Algebra A T]
    [IsScalarTower R A T] [Algebra.IsIntegral A T] :
    IsLocalization.Away (algebraMap R (integralClosure R T) d) T

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