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
theorem
IsIntegral.of_aeval_monic
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[CommRing A]
[Algebra R A]
{x : A}
{p : Polynomial R}
(monic : p.Monic)
(deg : p.natDegree ≠ 0)
(hx : IsIntegral R ((Polynomial.aeval x) p))
:
IsIntegral R x
theorem
IsIntegral.map_of_comp_eq
{R : Type u_5}
{S : Type u_6}
{T : Type u_7}
{U : Type u_8}
[CommRing R]
[Ring S]
[CommRing T]
[Ring U]
[Algebra R S]
[Algebra T U]
(φ : R →+* T)
(ψ : S →+* U)
(h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S))
{a : S}
(ha : IsIntegral R a)
:
IsIntegral T (ψ a)
@[simp]
theorem
isIntegral_algEquiv
{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)
{x : A}
:
IsIntegral R (f x) ↔ IsIntegral R x
theorem
IsIntegral.tower_top
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommRing R]
[CommRing A]
[Ring B]
[Algebra R A]
[Algebra R B]
[Algebra A B]
[IsScalarTower R A B]
{x : B}
(hx : IsIntegral R x)
:
IsIntegral A x
If R → A → B is an algebra tower,
then if the entire tower is an integral extension so is A → B.
theorem
RingEquiv.isIntegral_iff
{R : Type u_5}
{S : Type u_6}
{T : Type u_7}
[CommRing R]
[CommRing S]
[CommRing T]
[Algebra R S]
[Algebra T S]
(φ : R ≃+* T)
(h : (algebraMap T S).comp φ.toRingHom = algebraMap R S)
(a : S)
:
IsIntegral R a ↔ IsIntegral T a
theorem
map_isIntegral_int
{B : Type u_5}
{C : Type u_6}
{F : Type u_7}
[Ring B]
[Ring C]
{b : B}
[FunLike F B C]
[RingHomClass F B C]
(f : F)
(hb : IsIntegral ℤ b)
:
IsIntegral ℤ (f b)
theorem
IsIntegral.of_subring
{R : Type u_1}
{B : Type u_3}
[CommRing R]
[Ring B]
[Algebra R B]
{x : B}
(T : Subring R)
(hx : IsIntegral (↥T) x)
:
IsIntegral R x
theorem
IsIntegral.algebraMap
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommRing R]
[CommRing A]
[Ring B]
[Algebra R A]
[Algebra R B]
[Algebra A B]
[IsScalarTower R A B]
{x : A}
(h : IsIntegral R x)
:
IsIntegral R ((algebraMap A B) x)
theorem
isIntegral_algebraMap_iff
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[CommRing R]
[CommRing A]
[Ring B]
[Algebra R A]
[Algebra R B]
[Algebra A B]
[IsScalarTower R A B]
{x : A}
(hAB : Function.Injective ⇑(algebraMap A B))
:
IsIntegral R ((algebraMap A B) x) ↔ IsIntegral R x
theorem
isIntegral_iff_isIntegral_closure_finite
{R : Type u_1}
{B : Type u_3}
[CommRing R]
[Ring B]
[Algebra R B]
{r : B}
:
IsIntegral R r ↔ ∃ (s : Set R), s.Finite ∧ IsIntegral (↥(Subring.closure s)) r
theorem
fg_adjoin_of_finite
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[CommRing A]
[Algebra R A]
{s : Set A}
(hfs : s.Finite)
(his : ∀ x ∈ s, IsIntegral R x)
:
(Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
theorem
isNoetherian_adjoin_finset
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[CommRing A]
[Algebra R A]
[IsNoetherianRing R]
(s : Finset A)
(hs : ∀ x ∈ s, IsIntegral R x)
:
IsNoetherian R ↥(Algebra.adjoin R ↑s)