# 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`

- 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

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`

.

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_2}
[CommRing K]
[Algebra R K]
[ifr : IsFractionRing R K]
:

IsIntegralClosure R R K

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

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

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

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

@[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 = ⊥

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 }