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.

class IsIntegralClosure (A : Type u_1) (R : Type u_2) (B : Type u_3) [CommRing R] [CommSemiring A] [CommRing B] [Algebra R B] [Algebra A B] : Prop

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.

• algebraMap_injective : Function.Injective ⇑(algebraMap A B)
• isIntegral_iff {x : B} : IsIntegral R x ↔ ∃ (y : A), (algebraMap A B) y = x

@[deprecated IsIntegralClosure.algebraMap_injective (since := "2025-08-29")]

theorem IsIntegralClosure.algebraMap_injective' (A : Type u_1) (R : Type u_2) (B : Type u_3) {inst✝ : CommRing R} {inst✝¹ : CommSemiring A} {inst✝² : CommRing B} {inst✝³ : Algebra R B} {inst✝⁴ : Algebra A B} [self : IsIntegralClosure A R B] : Function.Injective ⇑(algebraMap A B)

Alias of IsIntegralClosure.algebraMap_injective.