Integral closure of a subring. #

If A is an R-algebra then a : A is integral over R if it is a root of a monic polynomial with coefficients in R. Enough theory is developed to 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.

RingHom.IsIntegralElem (f : R →+* A) (x : A) : x is integral with respect to the map f,
IsIntegral (x : A) : x is integral over R, i.e., is a root of a monic polynomial with coefficients in R.
integralClosure R A : the integral closure of R in A, regarded as a sub-R-algebra of A.

source

def RingHom.IsIntegralElem {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] (f : R →+* A) (x : A) :

Prop

An element x of A is said to be integral over R with respect to f if it is a root of a monic polynomial p : R[X] evaluated under f

Equations

RingHom.IsIntegralElem f x = ∃ (p : Polynomial R), Polynomial.Monic p ∧ Polynomial.eval₂ f x p = 0

Instances For

source

def RingHom.IsIntegral {R : Type u_1} {A : Type u_3} [CommRing R] [Ring A] (f : R →+* A) :

Prop

A ring homomorphism f : R →+* A is said to be integral if every element A is integral with respect to the map f

Equations

RingHom.IsIntegral f = ∀ (x : A), RingHom.IsIntegralElem f x

Instances For

source

def IsIntegral (R : Type u_1) {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] (x : A) :

Prop

An element x of an algebra A over a commutative ring R is said to be integral, if it is a root of some monic polynomial p : R[X]. Equivalently, the element is integral over R with respect to the induced algebraMap

Equations

IsIntegral R x = RingHom.IsIntegralElem (algebraMap R A) x

Instances For

source

def Algebra.IsIntegral (R : Type u_1) (A : Type u_3) [CommRing R] [Ring A] [Algebra R A] :

Prop

An algebra is integral if every element of the extension is integral over the base ring

Equations

Algebra.IsIntegral R A = ∀ (x : A), IsIntegral R x

Instances For

source

theorem RingHom.isIntegralElem_map {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] (f : R →+* S) {x : R} :

RingHom.IsIntegralElem f (f x)

source

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)

source

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)

source

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 : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)) {a : S} (ha : IsIntegral R a) :

IsIntegral T (ψ a)

source

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

source

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) (h : Algebra.IsIntegral R B) :

Algebra.IsIntegral R A

source

@[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

source

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.

source

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)

source

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

source

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)

source

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

source

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), Set.Finite s ∧ IsIntegral (↥(Subring.closure s)) r

source

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 : Polynomial.Monic f) (hfx : (Polynomial.aeval x) f = 0) :

Submodule.span R ↑(Finset.image (fun (x_1 : ℕ) => x ^ x_1) (Finset.range (Polynomial.natDegree f))) = Subalgebra.toSubmodule (Algebra.adjoin R {x})

source

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) :

Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {x}))

source

theorem fg_adjoin_of_finite {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {s : Set A} (hfs : Set.Finite s) (his : ∀ x ∈ s, IsIntegral R x) :

Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R s))

source

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)

source

theorem 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)

source

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

source

theorem 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

source

theorem IsIntegral.of_mem_of_fg {R : Type u_1} [CommRing R] {A : Type u_5} [Ring A] [Algebra R A] (S : Subalgebra R A) (HS : Submodule.FG (Subalgebra.toSubmodule S)) (x : A) (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.

source

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

source

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

source

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' : Submodule.FG N) (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.

source

theorem RingHom.Finite.to_isIntegral {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (h : RingHom.Finite f) :

RingHom.IsIntegral f

source

theorem RingHom.IsIntegral.of_finite {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (h : RingHom.Finite f) :

RingHom.IsIntegral f

Alias of RingHom.Finite.to_isIntegral.

source

theorem Algebra.IsIntegral.finite {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (h : Algebra.IsIntegral R A) [h' : Algebra.FiniteType R A] :

Module.Finite R A

The Kurosh problem asks to show that this is still true when A is not necessarily commutative and R is a field, but it has been solved in the negative. See https://arxiv.org/pdf/1706.02383.pdf for criteria for a finitely generated algebraic (= integral) algebra over a field to be finite dimensional.

source

theorem Algebra.finite_iff_isIntegral_and_finiteType {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] :

Module.Finite R A ↔ Algebra.IsIntegral R A ∧ Algebra.FiniteType R A

finite = integral + finite type

source

theorem RingHom.IsIntegral.to_finite {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (h : RingHom.IsIntegral f) (h' : RingHom.FiniteType f) :

RingHom.Finite f

source

theorem RingHom.Finite.of_isIntegral_of_finiteType {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} (h : RingHom.IsIntegral f) (h' : RingHom.FiniteType f) :

RingHom.Finite f

Alias of RingHom.IsIntegral.to_finite.

source

theorem RingHom.finite_iff_isIntegral_and_finiteType {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] {f : R →+* S} :

RingHom.Finite f ↔ RingHom.IsIntegral f ∧ RingHom.FiniteType f

finite = integral + finite type

source

theorem RingHom.IsIntegralElem.of_mem_closure {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} {z : S} (hx : RingHom.IsIntegralElem f x) (hy : RingHom.IsIntegralElem f y) (hz : z ∈ Subring.closure {x, y}) :

RingHom.IsIntegralElem f z

source

theorem IsIntegral.of_mem_closure {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} {z : A} (hx : IsIntegral R x) (hy : IsIntegral R y) (hz : z ∈ Subring.closure {x, y}) :

IsIntegral R z

source

theorem RingHom.isIntegralElem_zero {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] (f : R →+* B) :

RingHom.IsIntegralElem f 0

source

theorem isIntegral_zero {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] :

IsIntegral R 0

source

theorem RingHom.isIntegralElem_one {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] (f : R →+* B) :

RingHom.IsIntegralElem f 1

source

theorem isIntegral_one {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] :

IsIntegral R 1

source

theorem RingHom.IsIntegralElem.add {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} (hx : RingHom.IsIntegralElem f x) (hy : RingHom.IsIntegralElem f y) :

RingHom.IsIntegralElem f (x + y)

source

theorem IsIntegral.add {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) :

IsIntegral R (x + y)

source

theorem RingHom.IsIntegralElem.neg {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} (hx : RingHom.IsIntegralElem f x) :

RingHom.IsIntegralElem f (-x)

source

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)

source

theorem RingHom.IsIntegralElem.sub {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} (hx : RingHom.IsIntegralElem f x) (hy : RingHom.IsIntegralElem f y) :

RingHom.IsIntegralElem f (x - y)

source

theorem IsIntegral.sub {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) :

IsIntegral R (x - y)

source

theorem RingHom.IsIntegralElem.mul {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {x : S} {y : S} (hx : RingHom.IsIntegralElem f x) (hy : RingHom.IsIntegralElem f y) :

RingHom.IsIntegralElem f (x * y)

source

theorem IsIntegral.mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) :

IsIntegral R (x * y)

source

theorem IsIntegral.smul {B : Type u_3} {S : Type u_4} [Ring B] {R : Type u_5} [CommSemiring R] [CommRing S] [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)

source

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

source

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

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

Instances For

source

theorem mem_integralClosure_iff_mem_fg (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] {r : A} :

r ∈ integralClosure R A ↔ ∃ (M : Subalgebra R A), Submodule.FG (Subalgebra.toSubmodule M) ∧ r ∈ M

source

theorem adjoin_le_integralClosure {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} (hx : IsIntegral R x) :

Algebra.adjoin R {x} ≤ integralClosure R A

source

theorem le_integralClosure_iff_isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Subalgebra R A} :

S ≤ integralClosure R A ↔ Algebra.IsIntegral R ↥S

source

theorem Algebra.isIntegral_sup {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} :

Algebra.IsIntegral R ↥(S ⊔ T) ↔ Algebra.IsIntegral R ↥S ∧ Algebra.IsIntegral R ↥T

source

theorem integralClosure_map_algEquiv {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A ≃ₐ[R] S) :

Subalgebra.map (↑f) (integralClosure R A) = integralClosure R S

Mapping an integral closure along an AlgEquiv gives the integral closure.

source

def AlgHom.mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A →ₐ[R] S) :

↥(integralClosure R A) →ₐ[R] ↥(integralClosure R S)

An AlgHom between two rings restrict to an AlgHom between the integral closures inside them.

Equations

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

Instances For

source

@[simp]

theorem AlgHom.coe_mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A →ₐ[R] S) (x : ↥(integralClosure R A)) :

↑((AlgHom.mapIntegralClosure f) x) = f ↑x

source

def AlgEquiv.mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A ≃ₐ[R] S) :

↥(integralClosure R A) ≃ₐ[R] ↥(integralClosure R S)

An AlgEquiv between two rings restrict to an AlgEquiv between the integral closures inside them.

Equations

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

Instances For

source

@[simp]

theorem AlgEquiv.coe_mapIntegralClosure {R : Type u_1} {A : Type u_2} {S : Type u_4} [CommRing R] [CommRing A] [CommRing S] [Algebra R A] [Algebra R S] (f : A ≃ₐ[R] S) (x : ↥(integralClosure R A)) :

↑((AlgEquiv.mapIntegralClosure f) x) = f ↑x

source

theorem integralClosure.isIntegral {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (x : ↥(integralClosure R A)) :

IsIntegral R x

source

theorem IsIntegral.of_mul_unit {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x : B} {y : B} {r : R} (hr : (algebraMap R B) r * y = 1) (hx : IsIntegral R (x * y)) :

IsIntegral R x

source

theorem RingHom.IsIntegralElem.of_mul_unit {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (x : S) (y : S) (r : R) (hr : f r * y = 1) (hx : RingHom.IsIntegralElem f (x * y)) :

RingHom.IsIntegralElem f x

source

theorem IsIntegral.of_mem_closure' {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (G : Set A) (hG : ∀ x ∈ G, IsIntegral R x) (x : A) :

x ∈ Subring.closure G → IsIntegral R x

Generalization of IsIntegral.of_mem_closure bootstrapped up from that lemma

source

theorem IsIntegral.of_mem_closure'' {R : Type u_1} [CommRing R] {S : Type u_5} [CommRing S] {f : R →+* S} (G : Set S) (hG : ∀ x ∈ G, RingHom.IsIntegralElem f x) (x : S) :

x ∈ Subring.closure G → RingHom.IsIntegralElem f x

source

theorem IsIntegral.pow {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x : B} (h : IsIntegral R x) (n : ℕ) :

IsIntegral R (x ^ n)

source

theorem IsIntegral.nsmul {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x : B} (h : IsIntegral R x) (n : ℕ) :

IsIntegral R (n • x)

source

theorem IsIntegral.zsmul {R : Type u_1} {B : Type u_3} [CommRing R] [Ring B] [Algebra R B] {x : B} (h : IsIntegral R x) (n : ℤ) :

IsIntegral R (n • x)

source

theorem IsIntegral.multiset_prod {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) :

IsIntegral R (Multiset.prod s)

source

theorem IsIntegral.multiset_sum {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) :

IsIntegral R (Multiset.sum s)

source

theorem IsIntegral.prod {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {α : Type u_5} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) :

IsIntegral R (Finset.prod s fun (x : α) => f x)

source

theorem IsIntegral.sum {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {α : Type u_5} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) :

IsIntegral R (Finset.sum s fun (x : α) => f x)

source

theorem IsIntegral.det {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {n : Type u_5} [Fintype n] [DecidableEq n] {M : Matrix n n A} (h : ∀ (i j : n), IsIntegral R (M i j)) :

IsIntegral R (Matrix.det M)

source

@[simp]

theorem IsIntegral.pow_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : A} {n : ℕ} (hn : 0 < n) :

IsIntegral R (x ^ n) ↔ IsIntegral R x

source

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)

source

noncomputable def normalizeScaleRoots {R : Type u_1} [CommRing R] (p : Polynomial R) :

Polynomial R

The monic polynomial whose roots are p.leadingCoeff * x for roots x of p.

Equations

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

Instances For

source

theorem normalizeScaleRoots_coeff_mul_leadingCoeff_pow {R : Type u_1} [CommRing R] (p : Polynomial R) (i : ℕ) (hp : 1 ≤ Polynomial.natDegree p) :

Polynomial.coeff (normalizeScaleRoots p) i * Polynomial.leadingCoeff p ^ i = Polynomial.coeff p i * Polynomial.leadingCoeff p ^ (Polynomial.natDegree p - 1)

source

theorem leadingCoeff_smul_normalizeScaleRoots {R : Type u_1} [CommRing R] (p : Polynomial R) :

Polynomial.leadingCoeff p • normalizeScaleRoots p = Polynomial.scaleRoots p (Polynomial.leadingCoeff p)

source

theorem normalizeScaleRoots_support {R : Type u_1} [CommRing R] (p : Polynomial R) :

Polynomial.support (normalizeScaleRoots p) ≤ Polynomial.support p

source

theorem normalizeScaleRoots_degree {R : Type u_1} [CommRing R] (p : Polynomial R) :

Polynomial.degree (normalizeScaleRoots p) = Polynomial.degree p

source

theorem normalizeScaleRoots_eval₂_leadingCoeff_mul {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (p : Polynomial R) (h : 1 ≤ Polynomial.natDegree p) (f : R →+* S) (x : S) :

Polynomial.eval₂ f (f (Polynomial.leadingCoeff p) * x) (normalizeScaleRoots p) = f (Polynomial.leadingCoeff p) ^ (Polynomial.natDegree p - 1) * Polynomial.eval₂ f x p

source

theorem normalizeScaleRoots_monic {R : Type u_1} [CommRing R] (p : Polynomial R) (h : p ≠ 0) :

Polynomial.Monic (normalizeScaleRoots p)

source

theorem RingHom.isIntegralElem_leadingCoeff_mul {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (p : Polynomial R) (x : S) (h : Polynomial.eval₂ f x p = 0) :

RingHom.IsIntegralElem f (f (Polynomial.leadingCoeff p) * x)

Given a p : R[X] and a x : S such that p.eval₂ f x = 0, f p.leadingCoeff * x is integral.

source

theorem isIntegral_leadingCoeff_smul {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (p : Polynomial R) (x : S) [Algebra R S] (h : (Polynomial.aeval x) p = 0) :

IsIntegral R (Polynomial.leadingCoeff p • x)

Given a p : R[X] and a root x : S, then p.leadingCoeff • x : S is integral over R.

source

class IsIntegralClosure (A : Type u_1) (R : Type u_2) (B : Type u_3) [CommRing R] [CommSemiring A] [CommRing B] [Algebra R B] [Algebra A B] :

Prop

IsIntegralClosure A R B is the characteristic predicate stating A is the integral closure of R in B, i.e. that an element of B is integral over R iff it is an element of (the image of) A.

algebraMap_injective' : Function.Injective ⇑(algebraMap A B)
isIntegral_iff : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : A), (algebraMap A B) y = x

Instances

source

instance integralClosure.isIntegralClosure (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] :

IsIntegralClosure (↥(integralClosure R A)) R A

Equations

(_ : IsIntegralClosure (↥(integralClosure R A)) R A) = (_ : IsIntegralClosure (↥(integralClosure R A)) R A)

source

theorem IsIntegralClosure.algebraMap_injective (A : Type u_1) (R : Type u_2) (B : Type u_3) [CommRing R] [CommSemiring A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] :

Function.Injective ⇑(algebraMap A B)

source

theorem IsIntegralClosure.isIntegral (R : Type u_1) {A : Type u_2} (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] (x : A) :

IsIntegral R x

source

theorem IsIntegralClosure.isIntegral_algebra (R : Type u_1) {A : Type u_2} (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] :

Algebra.IsIntegral R A

source

theorem IsIntegralClosure.noZeroSMulDivisors (R : Type u_1) {A : Type u_2} (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] [NoZeroSMulDivisors R B] :

NoZeroSMulDivisors R A

source

noncomputable def IsIntegralClosure.mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (hx : IsIntegral R x) :

If x : B is integral over R, then it is an element of the integral closure of R in B.

Equations

IsIntegralClosure.mk' A x hx = Classical.choose (_ : ∃ (y : A), (algebraMap A B) y = x)

Instances For

source

@[simp]

theorem IsIntegralClosure.algebraMap_mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (hx : IsIntegral R x) :

(algebraMap A B) (IsIntegralClosure.mk' A x hx) = x

source

@[simp]

theorem IsIntegralClosure.mk'_one {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (h : optParam (IsIntegral R 1) (_ : IsIntegral R 1)) :

IsIntegralClosure.mk' A 1 h = 1

source

@[simp]

theorem IsIntegralClosure.mk'_zero {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (h : optParam (IsIntegral R 0) (_ : IsIntegral R 0)) :

IsIntegralClosure.mk' A 0 h = 0

source

theorem IsIntegralClosure.mk'_add {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :

IsIntegralClosure.mk' A (x + y) (_ : IsIntegral R (x + y)) = IsIntegralClosure.mk' A x hx + IsIntegralClosure.mk' A y hy

source

theorem IsIntegralClosure.mk'_mul {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (x : B) (y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :

IsIntegralClosure.mk' A (x * y) (_ : IsIntegral R (x * y)) = IsIntegralClosure.mk' A x hx * IsIntegralClosure.mk' A y hy

source

@[simp]

theorem IsIntegralClosure.mk'_algebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] [Algebra R A] [IsScalarTower R A B] (x : R) (h : optParam (IsIntegral R ((algebraMap R B) x)) (_ : IsIntegral R ((algebraMap R B) x))) :

IsIntegralClosure.mk' A ((algebraMap R B) x) h = (algebraMap R A) x

source

noncomputable def IsIntegralClosure.lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] {S : Type u_4} [CommRing S] [Algebra R S] [Algebra S B] [IsScalarTower R S B] [Algebra R A] [IsScalarTower R A B] (h : Algebra.IsIntegral R S) :

S →ₐ[R] A

If B / S / R is a tower of ring extensions where S is integral over R, then S maps (uniquely) into an integral closure B / A / R.

Equations

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

Instances For

source

@[simp]

theorem IsIntegralClosure.algebraMap_lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] {S : Type u_4} [CommRing S] [Algebra R S] [Algebra S B] [IsScalarTower R S B] [Algebra R A] [IsScalarTower R A B] (h : Algebra.IsIntegral R S) (x : S) :

(algebraMap A B) ((IsIntegralClosure.lift A B h) x) = (algebraMap S B) x

source

noncomputable def IsIntegralClosure.equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (A' : Type u_4) [CommRing A'] [Algebra A' B] [IsIntegralClosure A' R B] [Algebra R A] [Algebra R A'] [IsScalarTower R A B] [IsScalarTower R A' B] :

A ≃ₐ[R] A'

Integral closures are all isomorphic to each other.

Equations

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

Instances For

source

@[simp]

theorem IsIntegralClosure.algebraMap_equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommRing R] [CommRing A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] (A' : Type u_4) [CommRing A'] [Algebra A' B] [IsIntegralClosure A' R B] [Algebra R A] [Algebra R A'] [IsScalarTower R A B] [IsScalarTower R A' B] (x : A) :

(algebraMap A' B) ((IsIntegralClosure.equiv R A B A') x) = (algebraMap A B) x

source

theorem isIntegral_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Ring B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] (A_int : Algebra.IsIntegral R A) (x : B) (hx : IsIntegral A x) :

IsIntegral R x

If A is an R-algebra all of whose elements are integral over R, and x is an element of an A-algebra that is integral over A, then x is integral over R.

source

theorem Algebra.IsIntegral.trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Ring B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] (hA : Algebra.IsIntegral R A) (hB : Algebra.IsIntegral A B) :

Algebra.IsIntegral R B

If A is an R-algebra all of whose elements are integral over R, and B is an A-algebra all of whose elements are integral over A, then all elements of B are integral over R.

source

theorem RingHom.IsIntegral.trans {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (hf : RingHom.IsIntegral f) (hg : RingHom.IsIntegral g) :

RingHom.IsIntegral (RingHom.comp g f)

source

theorem RingHom.isIntegral_of_surjective {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) :

RingHom.IsIntegral f

source

theorem Algebra.isIntegral_of_surjective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (h : Function.Surjective ⇑(algebraMap R A)) :

Algebra.IsIntegral R A

source

theorem IsIntegral.tower_bot {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Ring B] [Algebra A B] [Algebra R B] [Algebra R A] [IsScalarTower R A B] (H : Function.Injective ⇑(algebraMap A B)) {x : A} (h : IsIntegral R ((algebraMap A B) x)) :

IsIntegral R x

If R → A → B is an algebra tower with A → B injective, then if the entire tower is an integral extension so is R → A

source

theorem RingHom.IsIntegral.tower_bot {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (hg : Function.Injective ⇑g) (hfg : RingHom.IsIntegral (RingHom.comp g f)) :

RingHom.IsIntegral f

source

theorem IsIntegral.tower_bot_of_field {R : Type u_6} {A : Type u_7} {B : Type u_8} [CommRing R] [Field A] [CommRing B] [Nontrivial B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} (h : IsIntegral R ((algebraMap A B) x)) :

IsIntegral R x

source

theorem RingHom.isIntegralElem.of_comp {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) {x : T} (h : RingHom.IsIntegralElem (RingHom.comp g f) x) :

RingHom.IsIntegralElem g x

source

theorem RingHom.IsIntegral.tower_top {R : Type u_1} {S : Type u_4} {T : Type u_5} [CommRing R] [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) (h : RingHom.IsIntegral (RingHom.comp g f)) :

RingHom.IsIntegral g

source

theorem RingHom.IsIntegral.quotient {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal S} (hf : RingHom.IsIntegral f) :

RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I))

source

theorem Algebra.IsIntegral.quotient {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {I : Ideal A} (hRA : Algebra.IsIntegral R A) :

Algebra.IsIntegral (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I)

source

theorem isIntegral_quotientMap_iff {R : Type u_1} {S : Type u_4} [CommRing R] [CommRing S] (f : R →+* S) {I : Ideal S} :

RingHom.IsIntegral (Ideal.quotientMap I f (_ : Ideal.comap f I ≤ Ideal.comap f I)) ↔ RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk I) f)

source

theorem isField_of_isIntegral_of_isField {R : Type u_6} {S : Type u_7} [CommRing R] [CommRing S] [Algebra R S] (H : Algebra.IsIntegral R S) (hRS : Function.Injective ⇑(algebraMap R S)) (hS : IsField S) :

IsField R

If the integral extension R → S is injective, and S is a field, then R is also a field.

source

theorem isField_of_isIntegral_of_isField' {R : Type u_6} {S : Type u_7} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] (H : Algebra.IsIntegral R S) (hR : IsField R) :

IsField S

source

theorem Algebra.IsIntegral.isField_iff_isField {R : Type u_6} {S : Type u_7} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] (H : Algebra.IsIntegral R S) (hRS : Function.Injective ⇑(algebraMap R S)) :

IsField R ↔ IsField S

source

theorem integralClosure_idem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] :

integralClosure (↑↑(integralClosure R A)) A = ⊥

source

instance instIsDomainSubtypeMemSubalgebraToCommSemiringToSemiringToCommSemiringInstMembershipInstSetLikeSubalgebraIntegralClosureToSemiring {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] :

IsDomain ↥(integralClosure R S)

Equations

(_ : IsDomain ↥(integralClosure R S)) = (_ : IsDomain ↥(integralClosure R S))

source

theorem roots_mem_integralClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] {f : Polynomial R} (hf : Polynomial.Monic f) {a : S} (ha : a ∈ Polynomial.aroots f S) :

a ∈ integralClosure R S

Documentation

Mathlib.RingTheory.IntegralClosure

Integral closure of a subring. #

Main definitions #