Documentation

Mathlib.RingTheory.IntegrallyClosed

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 #

Main results #

class IsIntegrallyClosed (R : Type u_1) [CommRing 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 xy, ↑(algebraMap R K) y = x

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

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

    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
    @[simp]