Integral closure of a subring.

Let A be an R-algebra. We prove that integral elements form a sub-R-algebra of A.

Main definitions

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

• integralClosure R A : the integral closure of R in an R-algebra A.

instance Module.End.isIntegral {R : Type u_1} [CommRing R] {M : Type u_5} [AddCommGroup M] [Module R M] [Module.Finite R M] : Algebra.IsIntegral R (Module.End R M)

Equations

• ⋯ = ⋯

theorem IsIntegral.of_finite (R : Type u_1) {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] [Module.Finite R B] (x : B) : IsIntegral R x

instance Algebra.IsIntegral.of_finite (R : Type u_1) (B : Type u_3) [CommRing R] [Ring B] [Algebra R B] [Module.Finite R B] : Algebra.IsIntegral R B

Equations

• ⋯ = ⋯

theorem IsIntegral.of_mem_of_fg {R : Type u_1} [CommRing R] {A : Type u_5} [Ring A] [Algebra R A] (S : Subalgebra R A) (HS : (Subalgebra.toSubmodule S).FG) (x : A) (hx : x ∈ S) : IsIntegral R x

If S is a sub-R-algebra of A and S is finitely-generated as an R-module, then all elements of S are integral over R.

theorem RingHom.IsIntegralElem.of_mem_closure {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} {z : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) (hz : z ∈ Subring.closure {x, y}) : f.IsIntegralElem z

theorem IsIntegral.of_mem_closure {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} {z : A} (hx : IsIntegral R x) (hy : IsIntegral R y) (hz : z ∈ Subring.closure {x, y}) : IsIntegral R z

theorem RingHom.IsIntegralElem.add {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x + y)

theorem IsIntegral.add {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x + y)

theorem RingHom.IsIntegralElem.neg {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} (hx : f.IsIntegralElem x) : f.IsIntegralElem (-x)

theorem IsIntegral.neg {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x : B} (hx : IsIntegral R x) : IsIntegral R (-x)

theorem RingHom.IsIntegralElem.sub {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x - y)

theorem IsIntegral.sub {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x - y)

theorem RingHom.IsIntegralElem.mul {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x * y)

theorem IsIntegral.mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x * y)

theorem IsIntegral.smul {B : Type u_3} {S : Type u_4} [Ring B] {R : Type u_5} [CommSemiring R] [CommRing S] [Algebra R B] [Algebra S B] [Algebra R S] [IsScalarTower R S B] {x : B} (r : R) (hx : IsIntegral S x) : IsIntegral S (r • x)

def integralClosure (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] : Subalgebra R A

The integral closure of R in an R-algebra A.

Equations

• integralClosure R A = { carrier := {r : A | IsIntegral R r}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }