mathlib documentation

ring_theory.algebraic

Algebraic elements and algebraic extensions #

An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial. An R-algebra is algebraic over R if and only if all its elements are algebraic over R. The main result in this file proves transitivity of algebraicity: a tower of algebraic field extensions is algebraic.

def is_algebraic (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] (x : A) :
Prop

An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial.

Equations
def transcendental (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] (x : A) :
Prop

An element of an R-algebra is transcendental over R if it is not algebraic over R.

Equations
def subalgebra.is_algebraic {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
Prop

A subalgebra is algebraic if all its elements are algebraic.

Equations
def algebra.is_algebraic (R : Type u) (A : Type v) [comm_ring R] [ring A] [algebra R A] :
Prop

An algebra is algebraic if all its elements are algebraic.

Equations
theorem subalgebra.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :

A subalgebra is algebraic if and only if it is algebraic an algebra.

theorem algebra.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] :

An algebra is algebraic if and only if it is algebraic as a subalgebra.

theorem is_integral.is_algebraic (R : Type u) {A : Type v} [comm_ring R] [nontrivial R] [ring A] [algebra R A] {x : A} (h : is_integral R x) :

An integral element of an algebra is algebraic.

theorem is_algebraic_algebra_map {R : Type u} {A : Type v} [comm_ring R] [nontrivial R] [ring A] [algebra R A] (a : R) :

An element of R is algebraic, when viewed as an element of the R-algebra A.

theorem is_algebraic_iff_is_integral (K : Type u) {A : Type v} [field K] [ring A] [algebra K A] {x : A} :

An element of an algebra over a field is algebraic if and only if it is integral.

theorem is_algebraic_iff_is_integral' (K : Type u) {A : Type v} [field K] [ring A] [algebra K A] :
theorem algebra.is_algebraic_trans {K : Type u_1} {L : Type u_2} {A : Type u_3} [field K] [field L] [comm_ring A] [algebra K L] [algebra L A] [algebra K A] [is_scalar_tower K L A] (L_alg : algebra.is_algebraic K L) (A_alg : algebra.is_algebraic L A) :

If L is an algebraic field extension of K and A is an algebraic algebra over L, then A is algebraic over K.

theorem algebra.is_algebraic_of_finite {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] [finite : finite_dimensional K L] :

A field extension is algebraic if it is finite.

theorem exists_integral_multiple {R : Type u_1} {S : Type u_2} [integral_domain R] [comm_ring S] [algebra R S] {z : S} (hz : is_algebraic R z) (inj : ∀ (x : R), (algebra_map R S) x = 0x = 0) :
∃ (x y : (integral_closure R S)) (H : y 0), z * y = x
theorem inv_eq_of_aeval_div_X_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] {x : L} {p : polynomial K} (aeval_ne : (polynomial.aeval x) p.div_X 0) :
theorem inv_eq_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] {x : L} {p : polynomial K} (aeval_eq : (polynomial.aeval x) p = 0) (coeff_zero_ne : p.coeff 0 0) :
theorem subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] (A : subalgebra K L) {x : A} {p : polynomial K} (aeval_eq : (polynomial.aeval x) p = 0) (coeff_zero_ne : p.coeff 0 0) :
theorem subalgebra.inv_mem_of_algebraic {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] (A : subalgebra K L) {x : A} (hx : is_algebraic K x) :
theorem subalgebra.is_field_of_algebraic {K : Type u_3} {L : Type u_4} [field K] [field L] [algebra K L] (A : subalgebra K L) (hKL : algebra.is_algebraic K L) :

In an algebraic extension L/K, an intermediate subalgebra is a field.