Module

LocalizationNormalIntegralClosure.lean

Nyll.SchemeTheory.RingTheory.Descent.LocalizationNormalIntegralClosure

1 declaration indexed from sourceView source ↗

Module documentation

Integral closure in a localization with normal boundary local rings

An integral fraction has locally divisible numerator at each maximal ideal. At a maximal ideal meeting the denominator submonoid, normality gives that divisibility in the prime localization. At the other maximal ideals the denominator is already a unit. Global divisibility then gives an element of the original ring. No principal denominator or noetherian hypothesis is used.

Imports6

Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.LocalProperties.Basic
Mathlib.RingTheory.Localization.Basic
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.FractionRing

Imported by3

theorem

isIntegrallyClosedIn_localization_of_normal_boundary

L35 ↗

SchemeTheory.isIntegrallyClosedIn_localization_of_normal_boundary

Documentation

A ring is integrally closed in a localization by non-zero-divisors if its local rings at maximal ideals meeting the denominator submonoid are normal.

Source context 4 commands

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

noncomputable section
namespace SchemeTheory
open scoped nonZeroDivisors
universe u v

Lean source · statement

theorem isIntegrallyClosedIn_localization_of_normal_boundary
    {R : Type u} [CommRing R] (M : Submonoid R) (hM : M ≤ R⁰)
    (T : Type v) [CommRing T] [Algebra R T] [IsLocalization M T]
    (hnormal : ∀ (p : Ideal R) [p.IsMaximal], (∃ s : M, (s : R) ∈ p) →
      IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)) :
    IsIntegrallyClosedIn R T

Module documentation

Integral closure in a localization with normal boundary local rings

Declarations

isIntegrallyClosedIn_localization_of_normal_boundary