mathlib3 documentation

ring_theory.algebraic

Algebraic elements and algebraic extensions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 a root of a nonzero polynomial with coefficients in R.

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
theorem is_transcendental_of_subsingleton (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] [subsingleton R] (x : A) :
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

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

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] [ring A] [algebra R A] [nontrivial R] {x : A} :

An integral element of an algebra is algebraic.

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

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] [algebra R A] [nontrivial R] :
theorem is_algebraic_nat {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] (n : ) :
theorem is_algebraic_int {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] (n : ) :
theorem is_algebraic_rat (R : Type u) {A : Type v} [division_ring A] [field R] [algebra R A] (n : ) :
theorem is_algebraic_of_mem_root_set {R : Type u} {A : Type v} [field R] [field A] [algebra R A] {p : polynomial R} {x : A} (hx : x p.root_set A) :
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] [algebra R A] [algebra R S] [algebra S A] [is_scalar_tower R S A] {a : S} :
theorem is_algebraic_alg_hom_of_is_algebraic {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {B : Type u_1} [ring B] [algebra R B] (f : A →ₐ[R] B) {a : A} (h : is_algebraic R 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] [algebra R A] {B : Type u_1} [ring B] [algebra R B] (e : A ≃ₐ[R] B) (h : algebra.is_algebraic R 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] [algebra R A] {B : Type u_1} [ring B] [algebra R 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] [algebra R A] [algebra R S] [algebra S A] [is_scalar_tower R S A] {a : S} (h : function.injective (algebra_map S A)) :
theorem is_algebraic_of_pow {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {r : A} {n : } (hn : 0 < n) (ht : is_algebraic R (r ^ n)) :
theorem transcendental.pow {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {r : A} (ht : transcendental R r) {n : } (hn : 0 < n) :
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.

@[protected]
theorem algebra.is_algebraic_trans {K : Type u_1} {L : Type u_2} {A : Type u_5} [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 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] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (hinj : function.injective (algebra_map R S)) {x : A} (A_alg : is_algebraic R 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.

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] [algebra K L] [algebra L A] [algebra K A] [is_scalar_tower K L A] {x : A} (A_alg : is_algebraic K 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] [algebra K L] [algebra L A] [algebra K A] [is_scalar_tower K L A] (A_alg : algebra.is_algebraic K 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] [algebra K L] [finite_dimensional K 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] [algebra K L] [finite : finite_dimensional K 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] [algebra K L] (ha : algebra.is_algebraic K L) (f : L →ₐ[K] L) :
theorem alg_hom.bijective {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] [finite_dimensional K 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] [algebra K L] (ha : algebra.is_algebraic K 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] [algebra K L] [finite_dimensional K 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] [algebra R S] {z : S} (hz : is_algebraic R z) (inj : (x : R), (algebra_map R S) x = 0 x = 0) :
(x : (integral_closure R S)) (y : R) (H : y 0), z * (algebra_map R 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] [algebra R S] [algebra S L] [algebra R L] [is_scalar_tower R S L] [is_integral_closure S R L] (h : algebra.is_algebraic R L) (inj : function.injective (algebra_map R 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] [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.

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 = polynomial.eval x p 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 = (polynomial.aeval 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') ((polynomial.aeval z) 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'), polynomial.eval z p