Integrally closed rings

An integrally closed ring R contains all the elements of Frac(R) that are integral over R. A special case of integrally closed rings are the Dedekind domains.

Main definitions

• IsIntegrallyClosedIn R A states R contains all integral elements of A
• IsIntegrallyClosed R states R contains all integral elements of Frac(R)

Main results

• isIntegrallyClosed_iff K, where K is a fraction field of R, states R is integrally closed iff it is the integral closure of R in K

TODO Related notions

The following definitions are closely related, especially in their applications in Mathlib.

A normal domain is a domain that is integrally closed in its field of fractions. Stacks: normal domain Normal domains are the major use case of IsIntegrallyClosed at the time of writing, and we have quite a few results that can be moved wholesale to a new NormalDomain definition. In fact, before PR https://github.com/leanprover-community/mathlib4/pull/6126 IsIntegrallyClosed was exactly defined to be a normal domain. (So you might want to copy some of its API when you define normal domains.)

A normal ring means that localizations at all prime ideals are normal domains. Stacks: normal ring This implies IsIntegrallyClosed, Stacks: Tag 034M but is equivalent to it only under some conditions (reduced + finitely many minimal primes), Stacks: Tag 030C in which case it's also equivalent to being a finite product of normal domains.

We'd need to add these conditions if we want exactly the products of Dedekind domains.

In fact noetherianity is sufficient to guarantee finitely many minimal primes, so IsDedekindRing could be defined as IsReduced, IsNoetherian, Ring.DimensionLEOne, and either IsIntegrallyClosed or NormalDomain. If we use NormalDomain then IsReduced is automatic, but we could also consider a version of NormalDomain that only requires the localizations are IsIntegrallyClosed but may not be domains, and that may not equivalent to the ring itself being IsIntegallyClosed (even for noetherian rings?).

@[reducible, inline]

abbrev IsIntegrallyClosedIn (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] : Prop

R is integrally closed in A if all integral elements of A are also elements of R.

Equations

• IsIntegrallyClosedIn R A = IsIntegralClosure R R A

@[reducible, inline]

abbrev IsIntegrallyClosed (R : Type u_1) [CommRing R] : Prop

R is integrally closed if all integral elements of Frac(R) are also elements of R.

This definition uses FractionRing R to denote Frac(R). See isIntegrallyClosed_iff if you want to choose another field of fractions for R.

Equations

• IsIntegrallyClosed R = IsIntegrallyClosedIn R (FractionRing R)

theorem AlgHom.isIntegrallyClosedIn {R : Type u_1} [CommRing R] {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) : IsIntegrallyClosedIn R B → IsIntegrallyClosedIn R A

Being integrally closed is preserved under injective algebra homomorphisms.

theorem AlgEquiv.isIntegrallyClosedIn {R : Type u_1} [CommRing R] {A : Type u_2} {B : Type u_3} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) : IsIntegrallyClosedIn R A ↔ IsIntegrallyClosedIn R B

Being integrally closed is preserved under algebra isomorphisms.

theorem isIntegrallyClosed_iff_isIntegrallyClosedIn {R : Type u_1} [CommRing R] (K : Type u_4) [CommRing K] [Algebra R K] [IsFractionRing R K] : IsIntegrallyClosed R ↔ IsIntegrallyClosedIn R K

R is integrally closed iff it is the integral closure of itself in its field of fractions.

theorem isIntegrallyClosed_iff_isIntegralClosure {R : Type u_1} [CommRing R] (K : Type u_4) [CommRing K] [Algebra R K] [IsFractionRing R K] : IsIntegrallyClosed R ↔ IsIntegralClosure R R K

R is integrally closed iff it is the integral closure of itself in its field of fractions.

theorem isIntegrallyClosedIn_iff {R : Type u_5} {A : Type u_6} [CommRing R] [CommRing A] [Algebra R A] : IsIntegrallyClosedIn R A ↔ Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ (y : R), (algebraMap R A) y = x

R is integrally closed in A iff all integral elements of A are also elements of R.

theorem isIntegrallyClosed_iff {R : Type u_1} [CommRing R] (K : Type u_4) [CommRing K] [Algebra R K] [IsFractionRing R K] : IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ (y : R), (algebraMap R K) y = x

R is integrally closed iff all integral elements of its fraction field K are also elements of R.

theorem IsIntegrallyClosedIn.algebraMap_eq_of_integral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [IsIntegrallyClosedIn R A] {x : A} : IsIntegral R x → ∃ (y : R), (algebraMap R A) y = x

theorem IsIntegrallyClosedIn.isIntegral_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [IsIntegrallyClosedIn R A] {x : A} : IsIntegral R x ↔ ∃ (y : R), (algebraMap R A) y = x

theorem IsIntegrallyClosedIn.exists_algebraMap_eq_of_isIntegral_pow {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [IsIntegrallyClosedIn R A] {x : A} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R (x ^ n)) : ∃ (y : R), (algebraMap R A) y = x

theorem IsIntegrallyClosedIn.exists_algebraMap_eq_of_pow_mem_subalgebra {R : Type u_1} [CommRing R] {A : Type u_3} [CommRing A] [Algebra R A] {S : Subalgebra R A} [IsIntegrallyClosedIn (↥S) A] {x : A} {n : ℕ} (hn : 0 < n) (hx : x ^ n ∈ S) : ∃ (y : ↥S), (algebraMap (↥S) A) y = x

theorem IsIntegrallyClosedIn.integralClosure_eq_bot_iff {R : Type u_1} (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] (hRA : Function.Injective ⇑(algebraMap R A)) : integralClosure R A = ⊥ ↔ IsIntegrallyClosedIn R A

@[simp]

theorem IsIntegrallyClosedIn.integralClosure_eq_bot (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [IsIntegrallyClosedIn R A] [NoZeroSMulDivisors R A] [Nontrivial A] : integralClosure R A = ⊥

theorem IsIntegrallyClosedIn.of_isIntegralClosure (R : Type u_1) {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_3} [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [IsIntegralClosure A R B] : IsIntegrallyClosedIn A B

If R is the integral closure of S in A, then it is integrally closed in A.

theorem IsIntegralClosure.of_isIntegrallyClosedIn {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_3} [CommRing B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] [IsIntegrallyClosedIn A B] [Algebra.IsIntegral R A] : IsIntegralClosure A R B

instance IsIntegrallyClosed.instIsIntegralClosure {R : Type u_1} [CommRing R] {K : Type u_3} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] [iic : IsIntegrallyClosed R] : IsIntegralClosure R R K

Note that this is not a duplicate instance, since IsIntegrallyClosed R is instead defined as IsIntegrallyClosed R R (FractionRing R).

theorem IsIntegrallyClosed.algebraMap_eq_of_integral {R : Type u_1} [CommRing R] {K : Type u_3} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] [IsIntegrallyClosed R] {x : K} : IsIntegral R x → ∃ (y : R), (algebraMap R K) y = x

theorem IsIntegrallyClosed.isIntegral_iff {R : Type u_1} [CommRing R] {K : Type u_3} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] [IsIntegrallyClosed R] {x : K} : IsIntegral R x ↔ ∃ (y : R), (algebraMap R K) y = x

theorem IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow {R : Type u_1} [CommRing R] {K : Type u_3} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] [IsIntegrallyClosed R] {x : K} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R (x ^ n)) : ∃ (y : R), (algebraMap R K) y = x

theorem IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra {R : Type u_1} [CommRing R] {K : Type u_4} [CommRing K] [Algebra R K] {S : Subalgebra R K} [IsIntegrallyClosed ↥S] [IsFractionRing (↥S) K] {x : K} {n : ℕ} (hn : 0 < n) (hx : x ^ n ∈ S) : ∃ (y : ↥S), (algebraMap (↥S) K) y = x

instance IsIntegralClosure.of_isIntegrallyClosed (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] (K : Type u_3) [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] [IsIntegrallyClosed R] [Algebra S R] [Algebra S K] [IsScalarTower S R K] [Algebra.IsIntegral S R] : IsIntegralClosure R S K

theorem IsIntegrallyClosed.integralClosure_eq_bot_iff {R : Type u_1} [CommRing R] (K : Type u_3) [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] : integralClosure R K = ⊥ ↔ IsIntegrallyClosed R

@[simp]

theorem IsIntegrallyClosed.pow_dvd_pow_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] {n : ℕ} (hn : n ≠ 0) {a b : R} : a ^ n ∣ b ^ n ↔ a ∣ b

@[simp]

theorem IsIntegrallyClosed.integralClosure_eq_bot (R : Type u_1) [CommRing R] (K : Type u_3) [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] [IsIntegrallyClosed R] : integralClosure R K = ⊥

This is almost a duplicate of IsIntegrallyClosedIn.integralClosure_eq_bot, except the NoZeroSMulDivisors hypothesis isn't inferred automatically from IsFractionRing.

theorem integralClosure.isIntegrallyClosedOfFiniteExtension {R : Type u_1} [CommRing R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {L : Type u_3} [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [IsDomain R] [FiniteDimensional K L] : IsIntegrallyClosed ↥(integralClosure R L)

theorem isIntegrallyClosed_of_isLocalization {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [IsIntegrallyClosed R] [IsDomain R] (M : Submonoid R) (hM : M ≤ nonZeroDivisors R) [IsLocalization M S] : IsIntegrallyClosed S

instance Field.instIsIntegrallyClosed (K : Type u_1) [Field K] : IsIntegrallyClosed K

Any field is integral closed.