Integral closure of a subring.
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.
Equations
- is_integral R x = ∃ (p : polynomial R), p.monic ∧ ⇑(polynomial.aeval x) p = 0
theorem
is_integral_algebra_map
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{x : R} :
is_integral R (⇑(algebra_map R A) x)
theorem
is_integral_alg_hom
{R : Type u}
{A : Type v}
{B : Type w}
[comm_ring R]
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra R B]
(f : A →ₐ[R] B)
{x : A} :
is_integral R x → is_integral R (⇑f x)
theorem
is_integral_of_is_scalar_tower
{R : Type u}
{A : Type v}
{B : Type w}
[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) :
is_integral R x → is_integral A x
theorem
is_integral_of_subring
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{x : A}
(T : set R)
[is_subring T] :
is_integral ↥T x → is_integral R x
theorem
is_integral_iff_is_integral_closure_finite
{R : Type u}
{A : Type v}
[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}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
(x : A) :
is_integral R x → ↑(algebra.adjoin R {x}).fg
theorem
fg_adjoin_of_finite
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{s : set A} :
s.finite → (∀ (x : A), x ∈ s → is_integral R x) → ↑(algebra.adjoin R s).fg
theorem
is_integral_of_noetherian'
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
(H : is_noetherian R A)
(x : A) :
is_integral R x
theorem
is_integral_of_noetherian
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
(S : subalgebra R A)
(H : is_noetherian R ↥↑S)
(x : A) :
x ∈ S → is_integral R x
theorem
is_integral_of_mem_of_fg
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
(S : subalgebra R A)
(HS : ↑S.fg)
(x : A) :
x ∈ S → is_integral R x
theorem
is_integral_of_mem_closure
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{x y z : A} :
is_integral R x → is_integral R y → z ∈ ring.closure {x, y} → is_integral R z
theorem
is_integral_zero
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A] :
is_integral R 0
theorem
is_integral_one
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A] :
is_integral R 1
theorem
is_integral_add
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{x y : A} :
is_integral R x → is_integral R y → is_integral R (x + y)
theorem
is_integral_neg
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{x : A} :
is_integral R x → is_integral R (-x)
theorem
is_integral_sub
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{x y : A} :
is_integral R x → is_integral R y → is_integral R (x - y)
theorem
is_integral_mul
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
{x y : A} :
is_integral R x → is_integral R y → is_integral R (x * y)
def
integral_closure
(R : Type u)
(A : Type v)
[comm_ring R]
[comm_ring A]
[algebra R A] :
subalgebra R A
Equations
- integral_closure R A = {carrier := {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)
(A : Type v)
[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.is_integral
{R : Type u}
{A : Type v}
[comm_ring R]
[comm_ring A]
[algebra R A]
(x : ↥(integral_closure R A)) :
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} :
p.monic → ⇑(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 : ∀ (x : A), is_integral R x)
(x : B) :
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]
(A_int : ∀ (x : A), is_integral R x)
(B_int : ∀ (x : B), is_integral A x)
(x : B) :
is_integral R x
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))
(x : A) :
is_integral R x
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} :
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_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} :
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
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 := _}