Theorems · Theorem · commutative algebra

IsIntegrallyClosed.of_localization

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (S : Set (PrimeSpectrum R)),
  (∀ p ∈ S, IsIntegrallyClosed (Localization.AtPrime p.asIdeal)) →
    ⨅ p ∈ S, Localization.subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯ = ⊥ → IsIntegrallyClosed R

An integral domain $R$ is integrally closed if there exists a set of prime ideals $S$ such that $\bigcap_{\mathfrak{p} \in S} R_{\mathfrak{p}} = R$ and for every $\mathfrak{p} \in S$, $R_{\mathfrak{p}}$ is integrally closed.

Defined in

Mathlib.RingTheory.LocalProperties.IntegrallyClosed

Cited by

1 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain