IsIntegrallyClosed is a local property

In this file, we prove that IsIntegrallyClosed is a local property.

Main results

• IsIntegrallyClosed.of_localization_maximal : An integral domain R is integral closed if Rₘ is integral closed for any maximal ideal m of R.

theorem IsIntegrallyClosed.iInf {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] {ι : Type u_3} (S : ι → Subalgebra R K) (h : ∀ (i : ι), IsIntegrallyClosed ↥(S i)) : IsIntegrallyClosed ↥(⨅ (i : ι), S i)

theorem IsIntegrallyClosed.of_iInf_eq_bot {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] {ι : Type u_3} (S : ι → Subalgebra R K) (h : ∀ (i : ι), IsIntegrallyClosed ↥(S i)) (hs : ⨅ (i : ι), S i = ⊥) : IsIntegrallyClosed R

theorem IsIntegrallyClosed.of_localization_submonoid {R : Type u_1} [CommRing R] [IsDomain R] {ι : Type u_3} (S : ι → Submonoid R) (h : ∀ (i : ι), S i ≤ nonZeroDivisors R) (hi : ∀ (i : ι), IsIntegrallyClosed (Localization (S i))) (hs : ⨅ (i : ι), Localization.subalgebra (FractionRing R) (S i) ⋯ = ⊥) : IsIntegrallyClosed R

theorem IsIntegrallyClosed.of_localization {R : Type u_1} [CommRing R] [IsDomain R] (S : Set (PrimeSpectrum R)) (h : ∀ p ∈ S, IsIntegrallyClosed (Localization.AtPrime p.asIdeal)) (hs : ⨅ 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.

theorem IsIntegrallyClosed.of_localization_maximal {R : Type u_1} [CommRing R] [IsDomain R] (h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)) : IsIntegrallyClosed R

An integral domain R is integral closed if Rₘ is integral closed for any maximal ideal m of R.

theorem isIntegrallyClosed_ofLocalizationMaximal : OfLocalizationMaximal fun (R : Type u_3) (x : CommRing R) => ∀ [IsDomain R], IsIntegrallyClosed R

theorem IsIntegrallyClosed.of_isLocalization_maximal {R : Type u_1} [CommRing R] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3) [(P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)] [(P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)] [∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] [IsDomain R] (h : ∀ (P : Ideal R) [inst : P.IsMaximal], IsIntegrallyClosed (Rₚ P)) : IsIntegrallyClosed R