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

source

class IsIntegrallyClosed (R : Type u_1) [CommRing R] :

Prop

algebraMap_eq_of_integral : ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, ↑(algebraMap R (FractionRing R)) y = x
All integral elements of Frac(R) are also elements of R.

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.

Instances

source

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, ↑(algebraMap R K) y = x

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

source

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.

source

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

IsIntegralClosure R R K

Equations

@IsIntegrallyClosed.instIsIntegralClosureToCommSemiring = @IsIntegrallyClosed.instIsIntegralClosureToCommSemiring.proof_1

source

theorem IsIntegrallyClosed.isIntegral_iff {R : Type u_1} [CommRing R] [iic : IsIntegrallyClosed R] {K : Type u_2} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] {x : K} :

IsIntegral R x ↔ ∃ y, ↑(algebraMap R K) y = x

source

theorem IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow {R : Type u_1} [CommRing R] [iic : IsIntegrallyClosed R] {K : Type u_2} [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] {x : K} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R (x ^ n)) :

∃ y, ↑(algebraMap R K) y = x

source

theorem IsIntegrallyClosed.exists_algebraMap_eq_of_pow_mem_subalgebra {R : Type u_1} [CommRing R] {K : Type u_3} [CommRing K] [Algebra R K] {S : Subalgebra R K} [IsIntegrallyClosed { x // x ∈ S }] [IsFractionRing { x // x ∈ S } K] {x : K} {n : ℕ} (hn : 0 < n) (hx : x ^ n ∈ S) :

∃ y, ↑(algebraMap { x // x ∈ S } K) y = x

source

theorem IsIntegrallyClosed.integralClosure_eq_bot_iff {R : Type u_1} [CommRing R] (K : Type u_2) [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] :

integralClosure R K = ⊥ ↔ IsIntegrallyClosed R

source

@[simp]

theorem IsIntegrallyClosed.integralClosure_eq_bot (R : Type u_1) [CommRing R] [iic : IsIntegrallyClosed R] (K : Type u_2) [CommRing K] [Algebra R K] [ifr : IsFractionRing R K] :

integralClosure R K = ⊥

source

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 { x // x ∈ integralClosure R L }