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 ofRin anR-algebraA.
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]
:
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)
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]
:
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.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
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
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
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
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' := ⋯ }
Instances For
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