Documentation

Mathlib.RingTheory.LocalProperties.IntegrallyClosed

IsIntegrallyClosed is a local property #

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

Main results #

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 = ) :
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) = ) :

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.

An integral domain R is integral closed if Rₘ is integral closed for any maximal ideal m of 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)) :