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} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] (S : Subalgebra R B) : Algebra.IsIntegral R ↥S ↔ ∀ x ∈ S, IsIntegral R x

instance Subalgebra.isIntegral {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] [Algebra.IsIntegral R B] (S : Subalgebra R B) : Algebra.IsIntegral R ↥S

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 Algebra.IsIntegral.of_surjective {R : Type u_1} [CommRing R] {A : Type u_5} {B : Type u_6} [Ring A] [Ring B] [Algebra R A] [Algebra R B] [Algebra.IsIntegral R A] (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) : Algebra.IsIntegral R B

Homomorphic image of an integral algebra is an integral algebra.

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 (End R M)

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

theorem Algebra.isIntegral_of_surjective {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] (H : Function.Surjective ⇑(algebraMap R B)) : Algebra.IsIntegral R B

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] [IsDomain A] {M : Type u_5} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [Module.IsTorsionFree 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

Stacks Tag 00GK

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.

---

Stacks Tag 00GK

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)

theorem isIntegral_intCast {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] (n : ℤ) : IsIntegral R ↑n

theorem isIntegral_natCast {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] (a : ℕ) : IsIntegral R ↑a

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

instance Algebra.IsIntegral.prod {R : Type u_1} [CommRing R] {A : Type u_5} {B : Type u_6} [Ring A] [Algebra R A] [Ring B] [Algebra R B] [Algebra.IsIntegral R A] [Algebra.IsIntegral R B] : Algebra.IsIntegral R (A × B)

Product of two integral algebras is an integral algebra.

theorem IsIntegral.tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Ring B] [Algebra R A] [Algebra R B] (x : A) {y : B} (h : IsIntegral R y) : IsIntegral A (x ⊗ₜ[R] y)

instance Algebra.IsIntegral.tensorProduct (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [int : Algebra.IsIntegral R B] : Algebra.IsIntegral A (TensorProduct R A B)

@[instance_reducible]

instance instMulSemiringActionSubtypeMemSubalgebraIntegralClosure {G : Type u_1} {R : Type u_2} {K : Type u_3} [CommRing R] [CommRing K] [Algebra R K] [Group G] [MulSemiringAction G K] [SMulCommClass G R K] : MulSemiringAction G ↥(integralClosure R K)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem integralClosure.coe_smul {G : Type u_1} {R : Type u_2} {K : Type u_3} [CommRing R] [CommRing K] [Algebra R K] [Group G] [MulSemiringAction G K] [SMulCommClass G R K] (g : G) (k : ↥(integralClosure R K)) : ↑(g • k) = g • ↑k

instance instSMulCommClassSubtypeMemSubalgebraIntegralClosure {G : Type u_1} {R : Type u_2} {K : Type u_3} [CommRing R] [CommRing K] [Algebra R K] [Group G] [MulSemiringAction G K] [SMulCommClass G R K] : SMulCommClass G R ↥(integralClosure R K)

instance instSMulDistribClassSubtypeMemSubalgebraIntegralClosure {G : Type u_1} {R : Type u_2} {K : Type u_3} [CommRing R] [CommRing K] [Algebra R K] [Group G] [MulSemiringAction G K] [SMulCommClass G R K] : SMulDistribClass G (↥(integralClosure R K)) K