doc-next-gen

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs

Module docstring

{"# Integral closure as a characteristic predicate

Main definitions

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

IsIntegralClosure R A : the characteristic predicate stating A is the integral closure of R in B, i.e. that an element of B is integral over R iff it is an element of (the image of) A. "}

IsIntegralClosure structure

(A R B : Type*) [CommRing R] [CommSemiring A] [CommRing B] [Algebra R B] [Algebra A B]

Full source

/-- `IsIntegralClosure A R B` is the characteristic predicate stating `A` is
the integral closure of `R` in `B`,
i.e. that an element of `B` is integral over `R` iff it is an element of (the image of) `A`.
-/
class IsIntegralClosure (A R B : Type*) [CommRing R] [CommSemiring A] [CommRing B] [Algebra R B]
  [Algebra A B] : Prop where
  algebraMap_injective' : Function.Injective (algebraMap A B)
  isIntegral_iff : ∀ {x : B}, IsIntegralIsIntegral R x ↔ ∃ y, algebraMap A B y = x

Integral Closure of a Commutative Ring in an Algebra

Informal description

The structure `IsIntegralClosure A R B` asserts that the commutative semiring `A` is the integral closure of the commutative ring `R` in the commutative ring `B`, where both `B` and `A` are equipped with an algebra structure over `R`. This means an element of `B` is integral over `R` if and only if it lies in the image of `A`.