Integral closure of a subring.

If A is an R-algebra then a : A is integral over R if it is a root of a monic polynomial with coefficients in R.

Main definitions

Let R be a CommRing and let A be an R-algebra.

• RingHom.IsIntegralElem (f : R →+* A) (x : A) : x is integral with respect to the map f,

• IsIntegral (x : A) : x is integral over R, i.e., is a root of a monic polynomial with coefficients in R.

def RingHom.IsIntegralElem {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] (f : R →+* A) (x : A) : Prop

An element x of A is said to be integral over R with respect to f if it is a root of a monic polynomial p : R[X] evaluated under f

Equations

• f.IsIntegralElem x = ∃ (p : Polynomial R), p.Monic ∧ Polynomial.eval₂ f x p = 0

def RingHom.IsIntegral {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] (f : R →+* A) : Prop

A ring homomorphism f : R →+* A is said to be integral if every element A is integral with respect to the map f

Equations

• f.IsIntegral = ∀ (x : A), f.IsIntegralElem x

def IsIntegral (R : Type u_1) {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] (x : A) : Prop

An element x of an algebra A over a commutative ring R is said to be integral, if it is a root of some monic polynomial p : R[X]. Equivalently, the element is integral over R with respect to the induced algebraMap

Equations

• IsIntegral R x = (algebraMap R A).IsIntegralElem x