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.faithfulSMul (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommSemiring A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] : FaithfulSMul A B