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

• 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

class 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.

• algebraMap_eq_of_integral : ∀ {x : FractionRing R}, IsIntegral R x → ∃ (y : R), (algebraMap R (FractionRing R)) y = x

  All integral elements of Frac(R) are also elements of R.

theorem isIntegrallyClosed_iff {R : Type u_1} [CommRing R] (K : Type u_2) [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 isIntegrallyClosed_iff_isIntegralClosure {R : Type u_1} [CommRing R] (K : Type u_2) [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.

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

Equations

• (_ : IsIntegralClosure R R K) = (_ : IsIntegralClosure R R K)

theorem IsIntegrallyClosed.isIntegral_iff {R : Type u_1} [CommRing R] [iic : IsIntegrallyClosed R] {K : Type u_3} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] {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] [iic : IsIntegrallyClosed R] {K : Type u_3} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] {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

theorem IsIntegralClosure.of_isIntegrallyClosed (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [iic : IsIntegrallyClosed R] (K : Type u_3) [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] [Algebra S R] [Algebra S K] [IsScalarTower S R K] (hRS : 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.integralClosure_eq_bot (R : Type u_1) [CommRing R] [iic : IsIntegrallyClosed R] (K : Type u_3) [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] : integralClosure R K = ⊥

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)