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.

source
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
source
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
source
theorem is_transcendental_of_subsingleton (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] [subsingleton R] (x : A) :
transcendental R x
source
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
source
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
source
theorem subalgebra.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [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 as an algebra.

source
theorem algebra.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [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_algebraic_iff_not_injective {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {x : A} :
is_algebraic R x ↔ ¬function.injective ⇑(polynomial.aeval x)
source
theorem is_integral.is_algebraic (R : Type u) {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] {x : A} :
is_integral R x → is_algebraic R x

An integral element of an algebra is algebraic.

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

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

source
theorem is_algebraic_one {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] :
is_algebraic R 1
source
theorem is_algebraic_nat {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] (n : ℕ) :
is_algebraic R ↑n
source
theorem is_algebraic_int {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [nontrivial R] (n : ℤ) :
is_algebraic R ↑n
source
theorem is_algebraic_rat (R : Type u) {A : Type v} [division_ring A] [field R] [char_zero R] [algebra R A] (n : ℚ) :
is_algebraic R ↑n
source
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} :
is_algebraic R a → is_algebraic R (⇑(algebra_map S A) a)
source
theorem is_algebraic_iff_is_integral {K : Type u} {A : Type v} [field K] [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
@[protected]
theorem algebra.is_algebraic_iff_is_integral {K : Type u} {A : Type v} [field K] [ring A] [algebra K A] :
algebra.is_algebraic K A ↔ algebra.is_integral K A
source
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) :
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 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) :
is_algebraic S 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.

source
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] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (hinj : function.injective ⇑(algebra_map R S)) (A_alg : algebra.is_algebraic R A) :
algebra.is_algebraic S 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.

source
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) :
is_algebraic L x

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

source
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) :
algebra.is_algebraic L A

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

source
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] :
algebra.is_integral K L

A field extension is integral if it is finite.

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} [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
source
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.

source
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 : K[X]} (aeval_ne : ⇑(polynomial.aeval x) p.div_X ≠ 0) :
x⁻¹ = ⇑(polynomial.aeval x) p.div_X / (⇑(polynomial.aeval x) p - ⇑(algebra_map K L) (p.coeff 0))
source
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 : K[X]} (aeval_eq : ⇑(polynomial.aeval x) p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) :
x⁻¹ = -(⇑(polynomial.aeval x) p.div_X / ⇑(algebra_map K L) (p.coeff 0))
source
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 : K[X]} (aeval_eq : ⇑(polynomial.aeval x) p = 0) (coeff_zero_ne : p.coeff 0 ≠ 0) :
(↑x)⁻¹ ∈ A
source
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) :
(↑x)⁻¹ ∈ A
source
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) :
is_field ↥A

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

source
def polynomial.has_scalar_pi (R' : Type u) (S' : Type v) [semiring R'] [has_scalar R' S'] :
has_scalar R'[X] (R' → S')

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

See the instance_diamonds test for details.

Equations
source
noncomputable def polynomial.has_scalar_pi' (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [semiring S'] [algebra R' S'] [has_scalar S' T'] :
has_scalar R'[X] (S' → T')

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

See the instance_diamonds test for details.

Equations
source
@[simp]
theorem polynomial_smul_apply (R' : Type u) (S' : Type v) [semiring R'] [has_scalar R' S'] (p : R'[X]) (f : R' → S') (x : R') :
(p • f) x = polynomial.eval x p • f x
source
@[simp]
theorem polynomial_smul_apply' (R' : Type u) (S' : Type v) (T' : Type w) [comm_semiring R'] [semiring S'] [algebra R' S'] [has_scalar S' T'] (p : R'[X]) (f : S' → T') (x : S') :
(p • f) x = ⇑(polynomial.aeval x) p • f x
source
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 R'[X] (S' → T')

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

Equations
source
@[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 R'[X] (S' → T')) = λ (p : R'[X]) (z : S'), ⇑(algebra_map S' T') (⇑(polynomial.aeval z) p)
source
@[simp]
theorem polynomial.algebra_map_pi_self_eq_eval (R' : Type u) [comm_semiring R'] :
⇑(algebra_map R'[X] (R' → R')) = λ (p : R'[X]) (z : R'), polynomial.eval z p