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 comm_ring and let A be an R-algebra.
ring_hom.is_integral_elem (f : R →+* A) (x : A):xis integral with respect to the mapf,is_integral (x : A):xis integral overR, i.e., is a root of a monic polynomial with coefficients inR.integral_closure R A: the integral closure ofRinA, regarded as a sub-R-algebra ofA.
def
ring_hom.is_integral_elem
{R : Type u_1}
{A : Type u_2}
[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 : polynomial R evaluated under f
Equations
- f.is_integral_elem x = ∃ (p : polynomial R), p.monic ∧ polynomial.eval₂ f x p = 0
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
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 : polynomial R.
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
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
theorem
is_integral_algebra_map
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
{x : R} :
is_integral R (⇑(algebra_map R A) x)
theorem
is_integral_of_noetherian
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
(H : is_noetherian R A)
(x : A) :
is_integral R x
theorem
is_integral_of_submodule_noetherian
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[ring A]
[algebra R A]
(S : subalgebra R A)
(H : is_noetherian R ↥↑S)
(x : A)
(hx : x ∈ S) :
is_integral R x
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)
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
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 : set R)
[is_subring T]
(hx : is_integral ↥T x) :
is_integral R x
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 ↥(ring.closure s) r
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}).fg
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).fg
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.fg)
(x : A)
(hx : x ∈ S) :
is_integral R x
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 ∈ ring.closure {x, y}) :
is_integral R z
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
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
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)
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)
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)
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)
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}, one_mem' := _, mul_mem' := _, zero_mem' := _, add_mem' := _, algebra_map_mem' := _}
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.fg ∧ r ∈ M
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.
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
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
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 : polynomial A}
(pmonic : p.monic)
(hp : ⇑(polynomial.aeval x) p = 0) :
is_integral ↥(algebra.adjoin R ↑(finsupp.frange (polynomial.map (algebra_map A B) p))) x
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.
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) :
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.
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)) :
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
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
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
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 (ideal.comap (algebra_map R A) I).quotient I.quotient
theorem
is_field_of_is_integral_of_is_field
{R : Type u_1}
{S : Type u_2}
[integral_domain R]
[integral_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
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 = ⊥
@[instance]
def
integral_closure.integral_domain
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[integral_domain S]
[algebra R S] :
Equations
- integral_closure.integral_domain = {add := comm_ring.add (subalgebra.comm_ring R S (integral_closure R S)), add_assoc := _, zero := comm_ring.zero (subalgebra.comm_ring R S (integral_closure R S)), zero_add := _, add_zero := _, neg := comm_ring.neg (subalgebra.comm_ring R S (integral_closure R S)), add_left_neg := _, add_comm := _, mul := comm_ring.mul (subalgebra.comm_ring R S (integral_closure R S)), mul_assoc := _, one := comm_ring.one (subalgebra.comm_ring R S (integral_closure R S)), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}