IsIntegrallyClosed is a local property #
In this file, we prove that IsIntegrallyClosed is a local property.
Main results #
IsIntegrallyClosed.of_localization_maximal: An integral domainRis integral closed ifRₘis integral closed for any maximal idealmofR.
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) ⋯ = ⊥)
:
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 ⋯ = ⊥)
:
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))
:
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