Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs

Module docstring

{"# 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. "}

RingHom.IsIntegralElem definition

(f : R →+* A) (x : A)

Full source

/-- 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` -/
def RingHom.IsIntegralElem (f : R →+* A) (x : A) :=
  ∃ p : R[X], Monic p ∧ eval₂ f x p = 0

Integral element with respect to a ring homomorphism

Informal description

An element \( x \) of an \( R \)-algebra \( A \) is integral over \( R \) with respect to a ring homomorphism \( f: R \to A \) if there exists a monic polynomial \( p \in R[X] \) such that evaluating \( p \) at \( x \) under \( f \) yields zero, i.e., \( p(x) = 0 \).

RingHom.IsIntegral definition

(f : R →+* A)

Full source

/-- A ring homomorphism `f : R →+* A` is said to be integral
if every element `A` is integral with respect to the map `f` -/
@[algebraize Algebra.IsIntegral.mk, stacks 00GI "(2)"]
def RingHom.IsIntegral (f : R →+* A) :=
  ∀ x : A, f.IsIntegralElem x

Integral ring homomorphism

Informal description

A ring homomorphism \( f: R \to A \) is called integral if every element \( x \) in \( A \) is integral over \( R \) with respect to \( f \), meaning that for each \( x \), there exists a monic polynomial \( p \in R[X] \) such that \( p(x) = 0 \) when evaluated under \( f \).

IsIntegral definition

(x : A) : Prop

Full source

/-- 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` -/
def IsIntegral (x : A) : Prop :=
  (algebraMap R A).IsIntegralElem x

Integral element over a commutative ring

Informal description

An element \( x \) of an \( R \)-algebra \( A \) is *integral* over \( R \) if it is a root of some monic polynomial \( p \in R[X] \) when evaluated under the canonical algebra map \( \text{algebraMap} : R \to A \). In other words, \( x \) satisfies \( p(x) = 0 \) for some monic polynomial \( p \) with coefficients in \( R \).