NYLL
Module

BoundaryNormalIntegralClosure.lean

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

Module documentation

Integral closure across a boundary with normal local rings

Only the local rings on the principal boundary need to be normal. An integral element of the localization has no pole there: normality proves local divisibility of its numerator, and divisibility descends from the localizations at maximal ideals. No normality away from the boundary is assumed.

Imports7
Imported by3

Declarations

theorem

isIntegrallyClosedIn_away_of_normal_boundary

L36 ↗
SchemeTheory.isIntegrallyClosedIn_away_of_normal_boundary
Documentation

A ring with normal local rings on V(d) is integrally closed in its localization away from the non-zero-divisor d.

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_away_of_normal_boundary
    {R : Type u} [CommRing R] (d : R) (hd : d ∈ R⁰)
    (T : Type v) [CommRing T] [Algebra R T] [IsLocalization.Away d T]
    (hnormal : ∀ (p : Ideal R) [p.IsMaximal], d ∈ p →
      IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)) :
    IsIntegrallyClosedIn R T
theorem

integralClosure_eq_finite_subalgebra_of_normal_boundary

L54 ↗
SchemeTheory.integralClosure_eq_finite_subalgebra_of_normal_boundary
Documentation

A finite subalgebra which recovers T after inverting d, and is normal on its boundary, is the actual relative integral closure. The inclusion in T supplies the non-zero-divisor condition automatically.

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 integralClosure_eq_finite_subalgebra_of_normal_boundary
    {R : Type u} {T : Type v} [CommRing R] [CommRing T] [Algebra R T]
    (C : Subalgebra R T) [Module.Finite R C]
    (d : C) [IsLocalization.Away d T]
    (hnormal : ∀ (p : Ideal C) [p.IsMaximal], d ∈ p →
      IsDomain (Localization.AtPrime p) ∧ IsIntegrallyClosed (Localization.AtPrime p)) :
    integralClosure R T = C

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