Documentation

Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Properties of integral elements. #

We prove basic properties of integral elements in a ring extension.

theorem RingHom.isIntegralElem_map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] (f : R →+* S) {x : R} :
f.IsIntegralElem (f x)
theorem isIntegral_algebraMap {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {x : R} :
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} :
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 RingHom.isIntegralElem_zero {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] (f : R →+* B) :
f.IsIntegralElem 0
theorem isIntegral_zero {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] :
theorem RingHom.isIntegralElem_one {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] (f : R →+* B) :
f.IsIntegralElem 1
theorem isIntegral_one {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] :
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)) :
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} :
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) :

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) :
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) :
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) :
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) :
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)) :
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 : xs, 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 : xs, IsIntegral R x) :