# Documentation

Mathlib.RingTheory.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 IsAlgebraic (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] (x : A) :

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

Instances For
def Transcendental (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] (x : A) :

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

Instances For
theorem is_transcendental_of_subsingleton (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] [] (x : A) :
def Subalgebra.IsAlgebraic {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (S : ) :

A subalgebra is algebraic if all its elements are algebraic.

Instances For
def Algebra.IsAlgebraic (R : Type u) (A : Type v) [] [Ring A] [Algebra R A] :

An algebra is algebraic if all its elements are algebraic.

Instances For
theorem Subalgebra.isAlgebraic_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (S : ) :
Algebra.IsAlgebraic R { x // x S }

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

theorem Algebra.isAlgebraic_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] :

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

theorem isAlgebraic_iff_not_injective {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {x : A} :
theorem IsIntegral.isAlgebraic (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] [] {x : A} :

An integral element of an algebra is algebraic.

theorem isAlgebraic_zero {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] :
theorem isAlgebraic_algebraMap {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] (x : R) :
IsAlgebraic R (↑() x)

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

theorem isAlgebraic_one {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] :
theorem isAlgebraic_nat {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] (n : ) :
theorem isAlgebraic_int {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] (n : ) :
theorem isAlgebraic_rat (R : Type u) {A : Type v} [] [] [Algebra R A] (n : ) :
theorem isAlgebraic_of_mem_rootSet {R : Type u} {A : Type v} [] [] [Algebra R A] {p : } {x : A} (hx : x ) :
theorem isAlgebraic_algebraMap_of_isAlgebraic {R : Type u} {S : Type u_1} {A : Type v} [] [] [Ring A] [Algebra R A] [Algebra R S] [Algebra S A] [] {a : S} :
IsAlgebraic R (↑() a)
theorem isAlgebraic_algHom_of_isAlgebraic {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {B : Type u_2} [Ring B] [Algebra R B] (f : A →ₐ[R] B) {a : A} (h : ) :
IsAlgebraic R (f a)

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

theorem AlgEquiv.isAlgebraic {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {B : Type u_2} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B) (h : ) :

Transfer Algebra.IsAlgebraic across an AlgEquiv.

theorem AlgEquiv.isAlgebraic_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {B : Type u_2} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B) :
theorem isAlgebraic_algebraMap_iff {R : Type u} {S : Type u_1} {A : Type v} [] [] [Ring A] [Algebra R A] [Algebra R S] [Algebra S A] [] {a : S} (h : Function.Injective ↑()) :
IsAlgebraic R (↑() a)
theorem isAlgebraic_of_pow {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : A} {n : } (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) :
theorem Transcendental.pow {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : A} (ht : ) {n : } (hn : 0 < n) :
theorem isAlgebraic_iff_isIntegral {K : Type u} {A : Type v} [] [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.isAlgebraic_iff_isIntegral {K : Type u} {A : Type v} [] [Ring A] [Algebra K A] :
theorem isAlgebraic_of_larger_base_of_injective {R : Type u_3} {S : Type u_4} {A : Type u_5} [] [] [Ring A] [Algebra R S] [Algebra S A] [Algebra R A] [] (hinj : Function.Injective ↑()) {x : A} (A_alg : ) :

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.isAlgebraic_of_larger_base_of_injective {R : Type u_3} {S : Type u_4} {A : Type u_5} [] [] [Ring A] [Algebra R S] [Algebra S A] [Algebra R A] [] (hinj : Function.Injective ↑()) (A_alg : ) :

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 isAlgebraic_of_larger_base {K : Type u_1} (L : Type u_2) {A : Type u_5} [] [] [Ring A] [Algebra K L] [Algebra L A] [Algebra K A] [] {x : A} (A_alg : ) :

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

theorem Algebra.isAlgebraic_of_larger_base {K : Type u_1} (L : Type u_2) {A : Type u_5} [] [] [Ring A] [Algebra K L] [Algebra L A] [Algebra K A] [] (A_alg : ) :

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

theorem isAlgebraic_of_finite (K : Type u_1) {A : Type u_5} [] [Ring A] [Algebra K A] (e : A) [] :
theorem Algebra.isAlgebraic_of_finite (K : Type u_1) (A : Type u_5) [] [Ring A] [Algebra K A] [] :

A field extension is algebraic if it is finite.

theorem Algebra.isAlgebraic_trans {K : Type u_1} {L : Type u_2} {A : Type u_5} [] [] [] [Algebra K L] [Algebra L A] [Algebra K A] [] (L_alg : ) (A_alg : ) :

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.IsAlgebraic.algHom_bijective {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] (ha : ) (f : L →ₐ[K] L) :
theorem AlgHom.bijective {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] [] (ϕ : L →ₐ[K] L) :
@[simp]
theorem Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply (K : Type u_1) (L : Type u_2) [] [] [Algebra K L] (ha : ) (ϕ : L →ₐ[K] L) :
↑() ϕ = AlgEquiv.ofBijective ϕ (_ : )
@[simp]
theorem Algebra.IsAlgebraic.algEquivEquivAlgHom_apply (K : Type u_1) (L : Type u_2) [] [] [Algebra K L] (ha : ) (ϕ : L ≃ₐ[K] L) :
↑() ϕ = ϕ
noncomputable def Algebra.IsAlgebraic.algEquivEquivAlgHom (K : Type u_1) (L : Type u_2) [] [] [Algebra K L] (ha : ) :
(L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

Instances For
@[reducible]
noncomputable def algEquivEquivAlgHom (K : Type u_1) (L : Type u_2) [] [] [Algebra K L] [] :
(L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

Instances For
theorem exists_integral_multiple {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] {z : S} (hz : ) (inj : ∀ (x : R), ↑() x = 0x = 0) :
x y x_1, z * ↑() y = x
theorem IsIntegralClosure.exists_smul_eq_mul {R : Type u_1} {S : Type u_2} [] [] [] {L : Type u_3} [] [Algebra R S] [Algebra S L] [Algebra R L] [] [] (h : ) (inj : Function.Injective ↑()) (a : S) {b : S} (hb : b 0) :
c d x, 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_divX_ne_zero {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] {x : L} {p : } (aeval_ne : ↑() () 0) :
x⁻¹ = ↑() () / (↑() p - ↑() ())
theorem inv_eq_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] {x : L} {p : } (aeval_eq : ↑() p = 0) (coeff_zero_ne : 0) :
x⁻¹ = -(↑() () / ↑() ())
theorem Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (A : ) {x : { x // x A }} {p : } (aeval_eq : ↑() p = 0) (coeff_zero_ne : 0) :
(x)⁻¹ A
theorem Subalgebra.inv_mem_of_algebraic {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (A : ) {x : { x // x A }} (hx : IsAlgebraic K x) :
(x)⁻¹ A
theorem Subalgebra.isField_of_algebraic {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (A : ) (hKL : ) :
IsField { x // x A }

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

def Polynomial.hasSMulPi (R' : Type u) (S' : Type v) [Semiring R'] [SMul R' S'] :
SMul () (R'S')

This is not an instance as it forms a diamond with Pi.instSMul.

See the instance_diamonds test for details.

Instances For
noncomputable def Polynomial.hasSMulPi' (R' : Type u) (S' : Type v) (T' : Type w) [] [Semiring S'] [Algebra R' S'] [SMul S' T'] :
SMul () (S'T')

This is not an instance as it forms a diamond with Pi.instSMul.

See the instance_diamonds test for details.

Instances For
@[simp]
theorem polynomial_smul_apply (R' : Type u) (S' : Type v) [Semiring R'] [SMul R' S'] (p : ) (f : R'S') (x : R') :
(Polynomial R' (R'S')) (R'S') instHSMul p f x = f x
@[simp]
theorem polynomial_smul_apply' (R' : Type u) (S' : Type v) (T' : Type w) [] [Semiring S'] [Algebra R' S'] [SMul S' T'] (p : ) (f : S'T') (x : S') :
(Polynomial R' (S'T')) (S'T') instHSMul p f x = ↑() p f x
noncomputable def Polynomial.algebraPi (R' : Type u) (S' : Type v) (T' : Type w) [] [] [] [Algebra R' S'] [Algebra S' T'] :
Algebra () (S'T')

This is not an instance for the same reasons as Polynomial.hasSMulPi'.

Instances For
@[simp]
theorem Polynomial.algebraMap_pi_eq_aeval (R' : Type u) (S' : Type v) (T' : Type w) [] [] [] [Algebra R' S'] [Algebra S' T'] :
↑(algebraMap () (S'T')) = fun p z => ↑(algebraMap ((fun x => S') p) T') (↑() p)
@[simp]
theorem Polynomial.algebraMap_pi_self_eq_eval (R' : Type u) [] :
↑(algebraMap () (R'R')) = fun p z =>