ring_theory.integral_closure

def ring_hom.is_integral_elem {R : Type u_1} {A : Type u_3} [comm_ring 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

f.is_integral_elem x = ∃ (p : R[X]), p.monic ∧ polynomial.eval₂ f x p = 0

source

def ring_hom.is_integral {R : Type u_1} {A : Type u_3} [comm_ring 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

f.is_integral = ∀ (x : A), f.is_integral_elem x

source

def is_integral (R : Type u_1) {A : Type u_3} [comm_ring 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 algebra_map

Equations

is_integral R x = (algebra_map R A).is_integral_elem x

source

def algebra.is_integral (R : Type u_1) (A : Type u_3) [comm_ring 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.is_integral R A = (algebra_map R A).is_integral

source

theorem ring_hom.is_integral_map {R : Type u_1} {S : Type u_2} [comm_ring R] [ring S] (f : R →+* S) {x : R} :

f.is_integral_elem (⇑f x)

source

theorem is_integral_algebra_map {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] [algebra R A] {x : R} :

is_integral R (⇑(algebra_map R A) x)

source

theorem is_integral_of_noetherian {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] [algebra R A] (H : is_noetherian R A) (x : A) :

is_integral R x

source

theorem is_integral_of_submodule_noetherian {R : Type u_1} {A : Type u_3} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) (H : is_noetherian R ↥(S.to_submodule)) (x : A) (hx : x ∈ S) :

is_integral R x

source

theorem is_integral_alg_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) {x : A} (hx : is_integral R x) :

is_integral R (⇑f x)

source

@[simp]

theorem is_integral_alg_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] (f : A ≃ₐ[R] B) {x : A} :

is_integral R (⇑f x) ↔ is_integral R x

source

theorem is_integral_of_is_scalar_tower {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [is_scalar_tower R A B] (x : B) (hx : is_integral R x) :

is_integral A x

source

theorem is_integral_of_subring {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x : A} (T : subring R) (hx : is_integral ↥T x) :

is_integral R x

source

theorem is_integral.algebra_map {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [is_scalar_tower R A B] {x : A} (h : is_integral R x) :

is_integral R (⇑(algebra_map A B) x)

source

theorem is_integral_algebra_map_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] [algebra A B] [is_scalar_tower R A B] {x : A} (hAB : function.injective ⇑(algebra_map A B)) :

is_integral R (⇑(algebra_map A B) x) ↔ is_integral R x

source

theorem is_integral_iff_is_integral_closure_finite {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {r : A} :

is_integral R r ↔ ∃ (s : set R), s.finite ∧ is_integral ↥(subring.closure s) r

source

theorem fg_adjoin_singleton_of_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (x : A) (hx : is_integral R x) :

(algebra.adjoin R {x}).to_submodule.fg

source

theorem fg_adjoin_of_finite {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {s : set A} (hfs : s.finite) (his : ∀ (x : A), x ∈ s → is_integral R x) :

(algebra.adjoin R s).to_submodule.fg

source

theorem is_noetherian_adjoin_finset {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] [is_noetherian_ring R] (s : finset A) (hs : ∀ (x : A), x ∈ s → is_integral R x) :

is_noetherian R ↥(algebra.adjoin R ↑s)

source

theorem is_integral_of_mem_of_fg {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (S : subalgebra R A) (HS : S.to_submodule.fg) (x : A) (hx : x ∈ S) :

is_integral 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 ring_hom.is_integral_of_mem_closure {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x y z : S} (hx : f.is_integral_elem x) (hy : f.is_integral_elem y) (hz : z ∈ subring.closure {x, y}) :

f.is_integral_elem z

source

theorem is_integral_of_mem_closure {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y z : A} (hx : is_integral R x) (hy : is_integral R y) (hz : z ∈ subring.closure {x, y}) :

is_integral R z

source

theorem ring_hom.is_integral_zero {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) :

f.is_integral_elem 0

source

theorem is_integral_zero {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :

is_integral R 0

source

theorem ring_hom.is_integral_one {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) :

f.is_integral_elem 1

source

theorem is_integral_one {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :

is_integral R 1

source

theorem ring_hom.is_integral_add {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x y : S} (hx : f.is_integral_elem x) (hy : f.is_integral_elem y) :

f.is_integral_elem (x + y)

source

theorem is_integral_add {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y : A} (hx : is_integral R x) (hy : is_integral R y) :

is_integral R (x + y)

source

theorem ring_hom.is_integral_neg {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x : S} (hx : f.is_integral_elem x) :

f.is_integral_elem (-x)

source

theorem is_integral_neg {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x : A} (hx : is_integral R x) :

is_integral R (-x)

source

theorem ring_hom.is_integral_sub {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x y : S} (hx : f.is_integral_elem x) (hy : f.is_integral_elem y) :

f.is_integral_elem (x - y)

source

theorem is_integral_sub {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y : A} (hx : is_integral R x) (hy : is_integral R y) :

is_integral R (x - y)

source

theorem ring_hom.is_integral_mul {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {x y : S} (hx : f.is_integral_elem x) (hy : f.is_integral_elem y) :

f.is_integral_elem (x * y)

source

theorem is_integral_mul {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y : A} (hx : is_integral R x) (hy : is_integral R y) :

is_integral R (x * y)

source

theorem is_integral_smul {R : Type u_1} {A : Type u_2} {S : Type u_4} [comm_ring R] [comm_ring A] [comm_ring S] [algebra R A] [algebra S A] [algebra R S] [is_scalar_tower R S A] {x : A} (r : R) (hx : is_integral S x) :

is_integral S (r • x)

source

def integral_closure (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] :

subalgebra R A

The integral closure of R in an R-algebra A.

Equations

integral_closure R A = {carrier := {r : A | is_integral R r}, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}

source

theorem mem_integral_closure_iff_mem_fg (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] {r : A} :

r ∈ integral_closure R A ↔ ∃ (M : subalgebra R A), M.to_submodule.fg ∧ r ∈ M

source

theorem adjoin_le_integral_closure {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x : A} (hx : is_integral R x) :

algebra.adjoin R {x} ≤ integral_closure R A

source

theorem le_integral_closure_iff_is_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {S : subalgebra R A} :

S ≤ integral_closure R A ↔ algebra.is_integral R ↥S

source

theorem is_integral_sup {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {S T : subalgebra R A} :

algebra.is_integral R ↥(S ⊔ T) ↔ algebra.is_integral R ↥S ∧ algebra.is_integral R ↥T

source

theorem integral_closure_map_alg_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B] (f : A ≃ₐ[R] B) :

(integral_closure R A).map ↑f = integral_closure R B

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

source

theorem integral_closure.is_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (x : ↥(integral_closure R A)) :

is_integral R x

source

theorem ring_hom.is_integral_of_is_integral_mul_unit {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) (x y : S) (r : R) (hr : (⇑f r) * y = 1) (hx : f.is_integral_elem (x * y)) :

f.is_integral_elem x

source

theorem is_integral_of_is_integral_mul_unit {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x y : A} {r : R} (hr : (⇑(algebra_map R A) r) * y = 1) (hx : is_integral R (x * y)) :

is_integral R x

source

theorem is_integral_of_mem_closure' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (G : set A) (hG : ∀ (x : A), x ∈ G → is_integral R x) (x : A) (H : x ∈ subring.closure G) :

is_integral R x

Generalization of is_integral_of_mem_closure bootstrapped up from that lemma

source

theorem is_integral_of_mem_closure'' {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] {f : R →+* S} (G : set S) (hG : ∀ (x : S), x ∈ G → f.is_integral_elem x) (x : S) (H : x ∈ subring.closure G) :

f.is_integral_elem x

source

theorem is_integral.pow {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x : A} (h : is_integral R x) (n : ℕ) :

is_integral R (x ^ n)

source

theorem is_integral.nsmul {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x : A} (h : is_integral R x) (n : ℕ) :

is_integral R (n • x)

source

theorem is_integral.zsmul {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {x : A} (h : is_integral R x) (n : ℤ) :

is_integral R (n • x)

source

theorem is_integral.multiset_prod {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {s : multiset A} (h : ∀ (x : A), x ∈ s → is_integral R x) :

is_integral R s.prod

source

theorem is_integral.multiset_sum {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {s : multiset A} (h : ∀ (x : A), x ∈ s → is_integral R x) :

is_integral R s.sum

source

theorem is_integral.prod {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {α : Type u_3} {s : finset α} (f : α → A) (h : ∀ (x : α), x ∈ s → is_integral R (f x)) :

is_integral R (∏ (x : α) in s, f x)

source

theorem is_integral.sum {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {α : Type u_3} {s : finset α} (f : α → A) (h : ∀ (x : α), x ∈ s → is_integral R (f x)) :

is_integral R (∑ (x : α) in s, f x)

source

theorem is_integral.det {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {n : Type u_3} [fintype n] [decidable_eq n] {M : matrix n n A} (h : ∀ (i j : n), is_integral R (M i j)) :

is_integral R M.det

source

noncomputable def normalize_scale_roots {R : Type u_1} [comm_ring R] (p : R[X]) :

R[X]

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

Equations

normalize_scale_roots p = ∑ (i : ℕ) in p.support, ⇑(polynomial.monomial i) (ite (i = p.nat_degree) 1 ((p.coeff i) * p.leading_coeff ^ (p.nat_degree - 1 - i)))

source

theorem normalize_scale_roots_coeff_mul_leading_coeff_pow {R : Type u_1} [comm_ring R] (p : R[X]) (i : ℕ) (hp : 1 ≤ p.nat_degree) :

((normalize_scale_roots p).coeff i) * p.leading_coeff ^ i = (p.coeff i) * p.leading_coeff ^ (p.nat_degree - 1)

source

theorem leading_coeff_smul_normalize_scale_roots {R : Type u_1} [comm_ring R] (p : R[X]) :

p.leading_coeff • normalize_scale_roots p = scale_roots p p.leading_coeff

source

theorem normalize_scale_roots_support {R : Type u_1} [comm_ring R] (p : R[X]) :

(normalize_scale_roots p).support ≤ p.support

source

theorem normalize_scale_roots_degree {R : Type u_1} [comm_ring R] (p : R[X]) :

(normalize_scale_roots p).degree = p.degree

source

theorem normalize_scale_roots_eval₂_leading_coeff_mul {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (p : R[X]) (h : 1 ≤ p.nat_degree) (f : R →+* S) (x : S) :

polynomial.eval₂ f ((⇑f p.leading_coeff) * x) (normalize_scale_roots p) = (⇑f p.leading_coeff ^ (p.nat_degree - 1)) * polynomial.eval₂ f x p

source

theorem normalize_scale_roots_monic {R : Type u_1} [comm_ring R] (p : R[X]) (h : p ≠ 0) :

(normalize_scale_roots p).monic

source

theorem ring_hom.is_integral_elem_leading_coeff_mul {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) (p : R[X]) (x : S) (h : polynomial.eval₂ f x p = 0) :

f.is_integral_elem ((⇑f p.leading_coeff) * x)

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

source

theorem is_integral_leading_coeff_smul {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (p : R[X]) (x : S) [algebra R S] (h : ⇑(polynomial.aeval x) p = 0) :

is_integral R (p.leading_coeff • x)

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

source

@[class]

structure is_integral_closure (A : Type u_1) (R : Type u_2) (B : Type u_3) [comm_ring R] [comm_semiring A] [comm_ring B] [algebra R B] [algebra A B] :

Prop

algebra_map_injective : function.injective ⇑(algebra_map A B)
is_integral_iff : ∀ {x : B}, is_integral R x ↔ ∃ (y : A), ⇑(algebra_map A B) y = x

is_integral_closure 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.

Instances

source

@[protected, instance]

def integral_closure.is_integral_closure (R : Type u_1) (A : Type u_2) [comm_ring R] [comm_ring A] [algebra R A] :

is_integral_closure ↥(integral_closure R A) R A

source

@[protected]

theorem is_integral_closure.is_integral (R : Type u_1) {A : Type u_2} (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] [algebra R A] [is_scalar_tower R A B] (x : A) :

is_integral R x

source

theorem is_integral_closure.is_integral_algebra (R : Type u_1) {A : Type u_2} (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] [algebra R A] [is_scalar_tower R A B] :

algebra.is_integral R A

source

noncomputable def is_integral_closure.mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] (x : B) (hx : is_integral R x) :

A

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

Equations

is_integral_closure.mk' A x hx = classical.some _

source

@[simp]

theorem is_integral_closure.algebra_map_mk' {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] (x : B) (hx : is_integral R x) :

⇑(algebra_map A B) (is_integral_closure.mk' A x hx) = x

source

@[simp]

theorem is_integral_closure.mk'_one {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] (h : is_integral R 1 := is_integral_one) :

is_integral_closure.mk' A 1 h = 1

source

@[simp]

theorem is_integral_closure.mk'_zero {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] (h : is_integral R 0 := is_integral_zero) :

is_integral_closure.mk' A 0 h = 0

source

@[simp]

theorem is_integral_closure.mk'_add {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] (x y : B) (hx : is_integral R x) (hy : is_integral R y) :

is_integral_closure.mk' A (x + y) _ = is_integral_closure.mk' A x hx + is_integral_closure.mk' A y hy

source

@[simp]

theorem is_integral_closure.mk'_mul {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] (x y : B) (hx : is_integral R x) (hy : is_integral R y) :

is_integral_closure.mk' A (x * y) _ = (is_integral_closure.mk' A x hx) * is_integral_closure.mk' A y hy

source

@[simp]

theorem is_integral_closure.mk'_algebra_map {R : Type u_1} (A : Type u_2) {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] [algebra R A] [is_scalar_tower R A B] (x : R) (h : is_integral R (⇑(algebra_map R B) x) := is_integral_algebra_map) :

is_integral_closure.mk' A (⇑(algebra_map R B) x) h = ⇑(algebra_map R A) x

source

noncomputable def is_integral_closure.lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] {S : Type u_4} [comm_ring S] [algebra R S] [algebra S B] [is_scalar_tower R S B] [algebra R A] [is_scalar_tower R A B] (h : algebra.is_integral 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

is_integral_closure.lift A B h = {to_fun := λ (x : S), is_integral_closure.mk' A (⇑(algebra_map S B) x) _, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem is_integral_closure.algebra_map_lift {R : Type u_1} (A : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] {S : Type u_4} [comm_ring S] [algebra R S] [algebra S B] [is_scalar_tower R S B] [algebra R A] [is_scalar_tower R A B] (h : algebra.is_integral R S) (x : S) :

⇑(algebra_map A B) (⇑(is_integral_closure.lift A B h) x) = ⇑(algebra_map S B) x

source

noncomputable def is_integral_closure.equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] (A' : Type u_4) [comm_ring A'] [algebra A' B] [is_integral_closure A' R B] [algebra R A] [algebra R A'] [is_scalar_tower R A B] [is_scalar_tower R A' B] :

A ≃ₐ[R] A'

Integral closures are all isomorphic to each other.

Equations

is_integral_closure.equiv R A B A' = alg_equiv.of_alg_hom (is_integral_closure.lift A' B _) (is_integral_closure.lift A B _) _ _

source

@[simp]

theorem is_integral_closure.algebra_map_equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_ring R] [comm_ring A] [comm_ring B] [algebra R B] [algebra A B] [is_integral_closure A R B] (A' : Type u_4) [comm_ring A'] [algebra A' B] [is_integral_closure A' R B] [algebra R A] [algebra R A'] [is_scalar_tower R A B] [is_scalar_tower R A' B] (x : A) :

⇑(algebra_map A' B) (⇑(is_integral_closure.equiv R A B A') x) = ⇑(algebra_map A B) x

source

theorem is_integral_trans_aux {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] (x : B) {p : A[X]} (pmonic : p.monic) (hp : ⇑(polynomial.aeval x) p = 0) :

is_integral ↥(algebra.adjoin R ↑((polynomial.map (algebra_map A B) p).frange)) x

source

theorem is_integral_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] [algebra R A] [is_scalar_tower R A B] (A_int : algebra.is_integral R A) (x : B) (hx : is_integral A x) :

is_integral 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.is_integral_trans {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] [algebra R A] [is_scalar_tower R A B] (hA : algebra.is_integral R A) (hB : algebra.is_integral A B) :

algebra.is_integral 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 ring_hom.is_integral_trans {R : Type u_1} {S : Type u_4} {T : Type u_5} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) (hf : f.is_integral) (hg : g.is_integral) :

(g.comp f).is_integral

source

theorem ring_hom.is_integral_of_surjective {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) :

f.is_integral

source

theorem is_integral_of_surjective {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (h : function.surjective ⇑(algebra_map R A)) :

algebra.is_integral R A

source

theorem is_integral_tower_bot_of_is_integral {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] [algebra R A] [is_scalar_tower R A B] (H : function.injective ⇑(algebra_map A B)) {x : A} (h : is_integral R (⇑(algebra_map A B) x)) :

is_integral 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 ring_hom.is_integral_tower_bot_of_is_integral {R : Type u_1} {S : Type u_4} {T : Type u_5} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) (hg : function.injective ⇑g) (hfg : (g.comp f).is_integral) :

f.is_integral

source

theorem is_integral_tower_bot_of_is_integral_field {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [field A] [comm_ring B] [nontrivial B] [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B] {x : A} (h : is_integral R (⇑(algebra_map A B) x)) :

is_integral R x

source

theorem ring_hom.is_integral_elem_of_is_integral_elem_comp {R : Type u_1} {S : Type u_4} {T : Type u_5} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) {x : T} (h : (g.comp f).is_integral_elem x) :

g.is_integral_elem x

source

theorem ring_hom.is_integral_tower_top_of_is_integral {R : Type u_1} {S : Type u_4} {T : Type u_5} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) (h : (g.comp f).is_integral) :

g.is_integral

source

theorem is_integral_tower_top_of_is_integral {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_ring R] [comm_ring A] [comm_ring B] [algebra A B] [algebra R B] [algebra R A] [is_scalar_tower R A B] {x : B} (h : is_integral R x) :

is_integral 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 ring_hom.is_integral_quotient_of_is_integral {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal S} (hf : f.is_integral) :

(I.quotient_map f le_rfl).is_integral

source

theorem is_integral_quotient_of_is_integral {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {I : ideal A} (hRA : algebra.is_integral R A) :

algebra.is_integral (R ⧸ ideal.comap (algebra_map R A) I) (A ⧸ I)

source

theorem is_integral_quotient_map_iff {R : Type u_1} {S : Type u_4} [comm_ring R] [comm_ring S] (f : R →+* S) {I : ideal S} :

(I.quotient_map f le_rfl).is_integral ↔ ((ideal.quotient.mk I).comp f).is_integral

source

theorem is_field_of_is_integral_of_is_field {R : Type u_1} {S : Type u_2} [comm_ring R] [nontrivial R] [comm_ring S] [is_domain S] [algebra R S] (H : algebra.is_integral R S) (hRS : function.injective ⇑(algebra_map R S)) (hS : is_field S) :

is_field R

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

source

theorem is_field_of_is_integral_of_is_field' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain S] [algebra R S] (H : algebra.is_integral R S) (hR : is_field R) :

is_field S

source

theorem is_integral.is_field_iff_is_field {R : Type u_1} {S : Type u_2} [comm_ring R] [nontrivial R] [comm_ring S] [is_domain S] [algebra R S] (H : algebra.is_integral R S) (hRS : function.injective ⇑(algebra_map R S)) :

is_field R ↔ is_field S

source

theorem integral_closure_idem {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] :

integral_closure ↥↑(integral_closure R A) A = ⊥

source

@[protected, instance]

def integral_closure.is_domain {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain S] [algebra R S] :

is_domain ↥(integral_closure R S)

mathlib documentation

Integral closure of a subring. #

Main definitions #