# 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.

Equations
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.

Equations
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.

Equations
• S.IsAlgebraic = xS,
Instances For
class Algebra.IsAlgebraic (R : Type u) (A : Type v) [] [Ring A] [Algebra R A] :

An algebra is algebraic if all its elements are algebraic.

• isAlgebraic : ∀ (x : A),
Instances
theorem Algebra.IsAlgebraic.isAlgebraic {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [self : ] (x : A) :
class Algebra.Transcendental (R : Type u) (A : Type v) [] [Ring A] [Algebra R A] :

An algebra is transcendental if some element is transcendental.

• transcendental : ∃ (x : A),
Instances
theorem Algebra.Transcendental.transcendental {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [self : ] :
∃ (x : A),
theorem Algebra.isAlgebraic_def {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] :
∀ (x : A),
theorem Algebra.transcendental_def {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] :
∃ (x : A),
theorem Subalgebra.isAlgebraic_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (S : ) :
S.IsAlgebraic

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

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 transcendental_iff_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.

instance Algebra.IsIntegral.isAlgebraic {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] [] :
Equations
• =
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 p.rootSet A) :
theorem IsAlgebraic.algebraMap {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 {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 in that it allows noncommutative intermediate rings A.

theorem isAlgebraic_algHom_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {B : Type u_2} [Ring B] [Algebra R B] (f : A →ₐ[R] B) (hf : ) {a : A} :
IsAlgebraic R (f a)
theorem Algebra.IsAlgebraic.of_injective {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {B : Type u_2} [Ring B] [Algebra R B] (f : A →ₐ[R] B) (hf : ) [] :
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) [] :

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.invOf {R : Type u} {S : Type u_1} [] [] [Algebra R S] {x : S} [] (h : ) :
theorem IsAlgebraic.invOf_iff {R : Type u} {S : Type u_1} [] [] [Algebra R S] {x : S} [] :
theorem IsAlgebraic.inv_iff {R : Type u} [] {K : Type u_2} [] [Algebra R K] {x : K} :
theorem IsAlgebraic.inv {R : Type u} [] {K : Type u_2} [] [Algebra R K] {x : K} :

Alias of the reverse direction of IsAlgebraic.inv_iff.

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.isIntegral {K : Type u} {A : Type v} [] [Ring A] [Algebra K A] {x : A} :

Alias of the forward direction of isAlgebraic_iff_isIntegral.

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

instance Algebra.IsAlgebraic.isIntegral {K : Type u} {A : Type v} [] [Ring A] [Algebra K A] [] :

This used to be an alias of Algebra.isAlgebraic_iff_isIntegral but that would make Algebra.IsAlgebraic K A an explicit parameter instead of instance implicit.

Equations
• =
theorem IsAlgebraic.tower_top_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.tower_top_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 ()) [] :

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

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) [] :
instance 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.

Equations
• =
theorem Algebra.IsAlgebraic.trans {K : Type u_1} {L : Type u_2} {A : Type u_5} [] [] [Ring A] [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] [] [] (f : L →ₐ[K] L) :
theorem Algebra.IsAlgebraic.algHom_bijective₂ {K : Type u_1} {L : Type u_2} {R : Type u_3} [] [] [Algebra K L] [] [] [Algebra K R] [] (f : L →ₐ[K] R) (g : R →ₐ[K] L) :
theorem Algebra.IsAlgebraic.bijective_of_isScalarTower {K : Type u_1} {L : Type u_2} {R : Type u_3} [] [] [Algebra K L] [] [] [] [Algebra K R] [Algebra L R] [] (f : R →ₐ[K] L) :
theorem Algebra.IsAlgebraic.bijective_of_isScalarTower' {K : Type u_1} {L : Type u_2} {R : Type u_3} [] [] [Algebra K L] [] [Algebra K R] [] [] [Algebra L R] [] (f : R →ₐ[K] L) :
@[simp]
theorem Algebra.IsAlgebraic.algEquivEquivAlgHom_apply (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] [] [] (ϕ : L →ₐ[K] L) :
.symm ϕ =
noncomputable def Algebra.IsAlgebraic.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

Equations
• = { toFun := fun (ϕ : L ≃ₐ[K] L) => ϕ, invFun := fun (ϕ : L →ₐ[K] L) => , left_inv := , right_inv := , map_mul' := }
Instances For
theorem AlgHom.bijective {K : Type u_1} {L : Type u_2} [] [] [Algebra K L] [] (ϕ : L →ₐ[K] L) :
@[reducible, inline]
noncomputable abbrev 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

Equations
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 : R), y 0 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] [] [] [] (inj : Function.Injective ()) (a : S) {b : S} (hb : b 0) :
∃ (c : S) (d : R), 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_divX_ne_zero {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] {x : L} {p : } (aeval_ne : () p.divX 0) :
x⁻¹ = () p.divX / (() p - () (p.coeff 0))
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 : p.coeff 0 0) :
x⁻¹ = -(() p.divX / () (p.coeff 0))
theorem Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (A : ) {x : A} {p : } (aeval_eq : () p = 0) (coeff_zero_ne : p.coeff 0 0) :
(x)⁻¹ A
theorem Subalgebra.inv_mem_of_algebraic {K : Type u_3} {L : Type u_4} [] [] [Algebra K L] (A : ) {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 : ) [] :
IsField 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.

Equations
• = { smul := fun (p : ) (f : R'S') (x : R') => f x }
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.

Equations
Instances For
@[simp]
theorem polynomial_smul_apply (R' : Type u) (S' : Type v) [Semiring R'] [SMul R' S'] (p : ) (f : R'S') (x : R') :
(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') :
(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'.

Equations
• One or more equations did not get rendered due to their size.
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 : S') => (algebraMap S' T') (() p)
@[simp]
theorem Polynomial.algebraMap_pi_self_eq_eval (R' : Type u) [] :
(algebraMap () (R'R')) = fun (p : ) (z : R') =>