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

theorem IsIntegralClosure.algebraMap_injective' {A : Type u_1} (R : Type u_2) {B : Type u_3} : ∀ {inst : CommRing R} {inst_1 : CommSemiring A} {inst_2 : CommRing B} {inst_3 : Algebra R B} {inst_4 : Algebra A B} [self : IsIntegralClosure A R B], Function.Injective ⇑(algebraMap A B)

theorem IsIntegralClosure.isIntegral_iff {A : Type u_1} {R : Type u_2} {B : Type u_3} : ∀ {inst : CommRing R} {inst_1 : CommSemiring A} {inst_2 : CommRing B} {inst_3 : Algebra R B} {inst_4 : Algebra A B} [self : IsIntegralClosure A R B] {x : B}, IsIntegral R x ↔ ∃ (y : A), (algebraMap A B) y = x