Properties of integral elements. #
We prove basic properties of integral elements in a ring extension.
theorem
isIntegral_algebraMap
{R : Type u_1}
{A : Type u_3}
[CommRing R]
[Ring A]
[Algebra R A]
{x : R}
:
IsIntegral R ((algebraMap R A) x)
theorem
IsIntegral.map
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[CommRing A]
[Algebra R A]
{B : Type u_5}
{C : Type u_6}
{F : Type u_7}
[Ring B]
[Ring C]
[Algebra R B]
[Algebra A B]
[Algebra R C]
[IsScalarTower R A B]
[Algebra A C]
[IsScalarTower R A C]
{b : B}
[FunLike F B C]
[AlgHomClass F A B C]
(f : F)
(hb : IsIntegral R b)
:
IsIntegral R (f b)
theorem
isIntegral_algHom_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]
(f : A →ₐ[R] B)
(hf : Function.Injective ⇑f)
{x : A}
:
IsIntegral R (f x) ↔ IsIntegral R x
theorem
Submodule.span_range_natDegree_eq_adjoin
{R : Type u_5}
{A : Type u_6}
[CommRing R]
[Semiring A]
[Algebra R A]
{x : A}
{f : Polynomial R}
(hf : f.Monic)
(hfx : (Polynomial.aeval x) f = 0)
:
Submodule.span R ↑(Finset.image (fun (x_1 : ℕ) => x ^ x_1) (Finset.range f.natDegree)) = Subalgebra.toSubmodule (Algebra.adjoin R {x})
theorem
IsIntegral.fg_adjoin_singleton
{R : Type u_1}
{B : Type u_3}
[CommRing R]
[Ring B]
[Algebra R B]
{x : B}
(hx : IsIntegral R x)
:
(Subalgebra.toSubmodule (Algebra.adjoin R {x})).FG
theorem
isIntegral_zero
{R : Type u_1}
{B : Type u_3}
[CommRing R]
[Ring B]
[Algebra R B]
:
IsIntegral R 0
theorem
isIntegral_one
{R : Type u_1}
{B : Type u_3}
[CommRing R]
[Ring B]
[Algebra R B]
:
IsIntegral R 1
theorem
IsIntegral.of_pow
{R : Type u_1}
{B : Type u_3}
[CommRing R]
[Ring B]
[Algebra R B]
{x : B}
{n : ℕ}
(hn : 0 < n)
(hx : IsIntegral R (x ^ n))
:
IsIntegral R x