# mathlibdocumentation

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] [ A] (x : A) :
Prop

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

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

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

Equations
theorem is_transcendental_of_subsingleton (R : Type u) {A : Type v} [comm_ring R] [ring A] [ A] [subsingleton R] (x : A) :
def subalgebra.is_algebraic {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (S : 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] [ A] :
Prop

An algebra is algebraic if all its elements are algebraic.

Equations
• = ∀ (x : A), x
theorem subalgebra.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (S : A) :

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

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

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

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

An integral element of an algebra is algebraic.

theorem is_algebraic_zero {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] [nontrivial R] :
0
theorem is_algebraic_algebra_map {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] [nontrivial R] (x : R) :
( A) x)

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

theorem is_algebraic_one {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] [nontrivial R] :
1
theorem is_algebraic_nat {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] [nontrivial R] (n : ) :
theorem is_algebraic_int {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] [nontrivial R] (n : ) :
theorem is_algebraic_rat (R : Type u) {A : Type v} [field R] [ A] (n : ) :
theorem is_algebraic_of_mem_root_set {R : Type u} {A : Type v} [field R] [field A] [ A] {p : polynomial R} {x : A} (hx : x p.root_set A) :
x
theorem is_algebraic_algebra_map_of_is_algebraic {R : Type u} {S : Type u_1} {A : Type v} [comm_ring R] [comm_ring S] [ring A] [ A] [ S] [ A] [ A] {a : S} :
a ( A) a)
theorem is_algebraic_alg_hom_of_is_algebraic {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {B : Type u_1} [ring B] [ B] (f : A →ₐ[R] B) {a : A} (h : a) :
(f a)

This is slightly more general than is_algebraic_algebra_map_of_is_algebraic in that it allows noncommutative intermediate rings A.

theorem alg_equiv.is_algebraic {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {B : Type u_1} [ring B] [ B] (e : A ≃ₐ[R] B) (h : A) :

Transfer algebra.is_algebraic across an alg_equiv.

theorem alg_equiv.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {B : Type u_1} [ring B] [ B] (e : A ≃ₐ[R] B) :
theorem is_algebraic_algebra_map_iff {R : Type u} {S : Type u_1} {A : Type v} [comm_ring R] [comm_ring S] [ring A] [ A] [ S] [ A] [ A] {a : S} (h : function.injective A)) :
( A) a) a
theorem is_algebraic_of_pow {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {r : A} {n : } (hn : 0 < n) (ht : (r ^ n)) :
r
theorem transcendental.pow {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {r : A} (ht : r) {n : } (hn : 0 < n) :
(r ^ n)
theorem is_algebraic_iff_is_integral {K : Type u} {A : Type v} [field K] [ring A] [ A] {x : A} :
x x

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

@[protected]
theorem algebra.is_algebraic_iff_is_integral {K : Type u} {A : Type v} [field K] [ring A] [ A] :
theorem algebra.is_algebraic_trans {K : Type u_1} {L : Type u_2} {A : Type u_5} [field K] [field L] [comm_ring A] [ L] [ A] [ A] [ A] (L_alg : L) (A_alg : 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 is_algebraic_of_larger_base_of_injective {R : Type u_3} {S : Type u_4} {A : Type u_5} [comm_ring R] [comm_ring S] [comm_ring A] [ S] [ A] [ A] [ A] (hinj : function.injective S)) {x : A} (A_alg : x) :
x

If x is algebraic over R, then x is algebraic over S when S is an extension of R, and the map from R to S is injective.

theorem algebra.is_algebraic_of_larger_base_of_injective {R : Type u_3} {S : Type u_4} {A : Type u_5} [comm_ring R] [comm_ring S] [comm_ring A] [ S] [ A] [ A] [ A] (hinj : function.injective S)) (A_alg : A) :

If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R, and the map from R to S is injective.

theorem is_algebraic_of_larger_base (K : Type u_1) (L : Type u_2) {A : Type u_5} [field K] [field L] [comm_ring A] [ L] [ A] [ A] [ A] {x : A} (A_alg : x) :
x

If x is a algebraic over K, then x is algebraic over L when L is an extension of K

theorem algebra.is_algebraic_of_larger_base (K : Type u_1) (L : Type u_2) {A : Type u_5} [field K] [field L] [comm_ring A] [ L] [ A] [ A] [ A] (A_alg : A) :

If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K

theorem algebra.is_integral_of_finite (K : Type u_1) (L : Type u_2) [field K] [field L] [ L] [ L] :

A field extension is integral if it is finite.

theorem algebra.is_algebraic_of_finite (K : Type u_1) (L : Type u_2) [field K] [field L] [ L] [finite : L] :

A field extension is algebraic if it is finite.

theorem algebra.is_algebraic.alg_hom_bijective {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] (ha : L) (f : L →ₐ[K] L) :
theorem alg_hom.bijective {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] [ L] (ϕ : L →ₐ[K] L) :
@[simp]
theorem algebra.is_algebraic.alg_equiv_equiv_alg_hom_apply (K : Type u_1) (L : Type u_2) [field K] [field L] [ L] (ha : L) (ϕ : L ≃ₐ[K] L) :
@[simp]
theorem algebra.is_algebraic.alg_equiv_equiv_alg_hom_symm_apply (K : Type u_1) (L : Type u_2) [field K] [field L] [ L] (ha : L) (ϕ : L →ₐ[K] L) :
ϕ =
noncomputable def algebra.is_algebraic.alg_equiv_equiv_alg_hom (K : Type u_1) (L : Type u_2) [field K] [field L] [ L] (ha : L) :
(L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

Equations
@[reducible]
noncomputable def alg_equiv_equiv_alg_hom (K : Type u_1) (L : Type u_2) [field K] [field L] [ L] [ L] :
(L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

Equations
theorem exists_integral_multiple {R : Type u_1} {S : Type u_2} [comm_ring R] [is_domain R] [comm_ring S] [ S] {z : S} (hz : z) (inj : ∀ (x : R), S) x = 0x = 0) :
∃ (x : S)) (y : R) (H : y 0), z * S) y = x
theorem is_integral_closure.exists_smul_eq_mul {R : Type u_1} {S : Type u_2} [comm_ring R] [is_domain R] [comm_ring S] {L : Type u_3} [field L] [ S] [ L] [ L] [ L] [ L] (h : L) (inj : function.injective L)) (a : S) {b : S} (hb : b 0) :
∃ (c : S) (d : R) (H : d 0), d a = b * c

A fraction (a : S) / (b : S) can be reduced to (c : S) / (d : R), if S is the integral closure of R in an algebraic extension L of R.

theorem inv_eq_of_aeval_div_X_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [ L] {x : L} {p : polynomial K} (aeval_ne : p.div_X 0) :
x⁻¹ = p.div_X / ( p - L) (p.coeff 0))
theorem inv_eq_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [ L] {x : L} {p : polynomial K} (aeval_eq : p = 0) (coeff_zero_ne : p.coeff 0 0) :
x⁻¹ = -( p.div_X / L) (p.coeff 0))
theorem subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [ L] (A : L) {x : A} {p : polynomial K} (aeval_eq : 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] [ L] (A : L) {x : A} (hx : x) :
theorem subalgebra.is_field_of_algebraic {K : Type u_3} {L : Type u_4} [field K] [field L] [ L] (A : L) (hKL : L) :

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

def polynomial.has_smul_pi (R' : Type u) (S' : Type v) [semiring R'] [has_smul R' S'] :
has_smul (polynomial R') (R' → S')

This is not an instance as it forms a diamond with pi.has_smul.

See the instance_diamonds test for details.

Equations
noncomputable def polynomial.has_smul_pi' (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [semiring S'] [algebra R' S'] [has_smul S' T'] :
has_smul (polynomial R') (S' → T')

This is not an instance as it forms a diamond with pi.has_smul.

See the instance_diamonds test for details.

Equations
@[simp]
theorem polynomial_smul_apply (R' : Type u) (S' : Type v) [semiring R'] [has_smul R' S'] (p : polynomial R') (f : R' → S') (x : R') :
(p f) x = f x
@[simp]
theorem polynomial_smul_apply' (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [semiring S'] [algebra R' S'] [has_smul S' T'] (p : polynomial R') (f : S' → T') (x : S') :
(p f) x = p f x
noncomputable def polynomial.algebra_pi (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [comm_semiring S'] [comm_semiring T'] [algebra R' S'] [algebra S' T'] :
algebra (polynomial R') (S' → T')

This is not an instance for the same reasons as polynomial.has_smul_pi'.

Equations
@[simp]
theorem polynomial.algebra_map_pi_eq_aeval (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [comm_semiring S'] [comm_semiring T'] [algebra R' S'] [algebra S' T'] :
(algebra_map (polynomial R') (S' → T')) = λ (p : polynomial R') (z : S'), (algebra_map S' T') ( p)
@[simp]
theorem polynomial.algebra_map_pi_self_eq_eval (R' : Type u) [comm_semiring R'] :
(algebra_map (polynomial R') (R' → R')) = λ (p : polynomial R') (z : R'),