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] [comm_ring A] [algebra R A] :
A → Prop

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

Equations
def subalgebra.is_algebraic {R : Type u} {A : Type v} [comm_ring R] [comm_ring A] [algebra R A] :
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] [comm_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] [comm_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] [comm_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] [comm_ring A] [algebra R A] {x : A} :

An integral element of an algebra is algebraic.

theorem is_algebraic_iff_is_integral (K : Type u) {A : Type v} [field K] [comm_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 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] :

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} :
is_algebraic R z(∀ (x : R), (algebra_map R S) x = 0x = 0)(∃ (x y : (integral_closure R S)) (H : y 0), z * y = x)