Documentation

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs

Integral closure as a characteristic predicate #

Main definitions #

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

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] :

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.

Instances
    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