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.

theorem Subalgebra.isIntegral_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) : Algebra.IsIntegral R ↥S ↔ ∀ x ∈ S, IsIntegral R x

theorem Algebra.IsIntegral.of_injective {R : Type u_1} [CommRing R] {A : Type u_5} {B : Type u_6} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) [Algebra.IsIntegral R B] : Algebra.IsIntegral R A

theorem AlgEquiv.isIntegral_iff {R : Type u_1} [CommRing R] {A : Type u_5} {B : Type u_6} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) : Algebra.IsIntegral R A ↔ Algebra.IsIntegral R B

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

theorem isIntegral_of_noetherian {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] : IsNoetherian 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} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] (S : Subalgebra R B) (HS : (Subalgebra.toSubmodule S).FG) (x : B) (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 isIntegral_of_submodule_noetherian {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] (S : Subalgebra R B) (H : IsNoetherian R ↥(Subalgebra.toSubmodule S)) (x : B) (hx : x ∈ S) : IsIntegral R x

theorem isIntegral_of_smul_mem_submodule {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_5} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors A M] (N : Submodule R M) (hN : N ≠ ⊥) (hN' : N.FG) (x : A) (hx : ∀ n ∈ N, x • n ∈ N) : IsIntegral R x

Suppose A is an R-algebra, M is an A-module such that a • m ≠ 0 for all non-zero a and m. If x : A fixes a nontrivial f.g. R-submodule N of M, then x is R-integral.

theorem RingHom.Finite.to_isIntegral {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (h : f.Finite) : f.IsIntegral

theorem RingHom.IsIntegral.of_finite {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (h : f.Finite) : f.IsIntegral

Alias of RingHom.Finite.to_isIntegral.

theorem RingHom.IsIntegralElem.of_mem_closure {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x y 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 y 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 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 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 RingHom.IsIntegralElem.of_neg {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} (h : f.IsIntegralElem (-x)) : f.IsIntegralElem x

@[simp]

theorem RingHom.IsIntegralElem.neg_iff {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} : 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 IsIntegral.of_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

@[simp]

theorem IsIntegral.neg_iff {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x : B} : 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 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 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 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 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] [CommRing S] {R : Type u_5} [CommSemiring R] [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' := ⋯ }

theorem mem_integralClosure_iff (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] {a : A} : a ∈ integralClosure R A ↔ IsIntegral R a