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.

source

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

is_algebraic R x = ∃ (p : polynomial R), p ≠ 0 ∧ ⇑(polynomial.aeval x) p = 0

source

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

S.is_algebraic = ∀ (x : A), x ∈ S → is_algebraic R x

source

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

algebra.is_algebraic R A = ∀ (x : A), is_algebraic R x

source

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

S.is_algebraic ↔ algebra.is_algebraic R ↥S

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

source

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

algebra.is_algebraic R A ↔ ⊤.is_algebraic

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

source

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

is_integral R x → is_algebraic R x

An integral element of an algebra is algebraic.

source

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

is_algebraic K x ↔ is_integral K x

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

source

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] :

algebra.is_algebraic K L → algebra.is_algebraic L A → algebra.is_algebraic K A

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

source

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] :

algebra.is_algebraic K L

A field extension is algebraic if it is finite.

source

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 = 0 → x = 0) → (∃ (x y : ↥(integral_closure R S)) (H : y ≠ 0), z * ↑y = ↑x)

mathlib documentation

ring_theory.algebraic

Algebraic elements and algebraic extensions

General documentation

Additional documentation

Library

mathlib documentation

ring_theory.​algebraic

Algebraic elements and algebraic extensions

General documentation

Additional documentation

Library

ring_theory.algebraic