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

def Transcendental (R : Type u) {A : Type v} [CommRing 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.

theorem is_transcendental_of_subsingleton (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Subsingleton R] (x : A) : Transcendental R x

def Subalgebra.IsAlgebraic {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : Prop

A subalgebra is algebraic if all its elements are algebraic.

def Algebra.IsAlgebraic (R : Type u) (A : Type v) [CommRing R] [Ring A] [Algebra R A] : Prop

An algebra is algebraic if all its elements are algebraic.

theorem Subalgebra.isAlgebraic_iff {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : Subalgebra.IsAlgebraic 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} [CommRing R] [Ring A] [Algebra R A] : Algebra.IsAlgebraic R A ↔ Subalgebra.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} [CommRing R] [Ring A] [Algebra R A] {x : A} : IsAlgebraic R x ↔ ¬Function.Injective ↑(Polynomial.aeval x)

theorem IsIntegral.isAlgebraic (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] {x : A} : IsIntegral R x → IsAlgebraic R x

An integral element of an algebra is algebraic.

theorem isAlgebraic_zero {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] : IsAlgebraic R 0

theorem isAlgebraic_algebraMap {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] (x : R) : IsAlgebraic R (↑(algebraMap R A) 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} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] : IsAlgebraic R 1

theorem isAlgebraic_nat {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] (n : ℕ) : IsAlgebraic R ↑n

theorem isAlgebraic_int {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [Nontrivial R] (n : ℤ) : IsAlgebraic R ↑n

theorem isAlgebraic_rat (R : Type u) {A : Type v} [DivisionRing A] [Field R] [Algebra R A] (n : ℚ) : IsAlgebraic R ↑n

theorem isAlgebraic_of_mem_rootSet {R : Type u} {A : Type v} [Field R] [Field A] [Algebra R A] {p : Polynomial R} {x : A} (hx : x ∈ Polynomial.rootSet p A) : IsAlgebraic R x

theorem isAlgebraic_algebraMap_of_isAlgebraic {R : Type u} {S : Type u_1} {A : Type v} [CommRing R] [CommRing S] [Ring A] [Algebra R A] [Algebra R S] [Algebra S A] [IsScalarTower R S A] {a : S} : IsAlgebraic R a → IsAlgebraic R (↑(algebraMap S A) a)

theorem isAlgebraic_algHom_of_isAlgebraic {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {B : Type u_2} [Ring B] [Algebra R B] (f : A →ₐ[R] B) {a : A} (h : IsAlgebraic R a) : 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} [CommRing R] [Ring A] [Algebra R A] {B : Type u_2} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B) (h : Algebra.IsAlgebraic R A) : Algebra.IsAlgebraic R B

Transfer Algebra.IsAlgebraic across an AlgEquiv.

theorem AlgEquiv.isAlgebraic_iff {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {B : Type u_2} [Ring B] [Algebra R B] (e : A ≃ₐ[R] B) : Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R B

theorem isAlgebraic_algebraMap_iff {R : Type u} {S : Type u_1} {A : Type v} [CommRing R] [CommRing S] [Ring A] [Algebra R A] [Algebra R S] [Algebra S A] [IsScalarTower R S A] {a : S} (h : Function.Injective ↑(algebraMap S A)) : IsAlgebraic R (↑(algebraMap S A) a) ↔ IsAlgebraic R a

theorem isAlgebraic_of_pow {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {r : A} {n : ℕ} (hn : 0 < n) (ht : IsAlgebraic R (r ^ n)) : IsAlgebraic R r

theorem Transcendental.pow {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {r : A} (ht : Transcendental R r) {n : ℕ} (hn : 0 < n) : Transcendental R (r ^ n)

theorem isAlgebraic_iff_isIntegral {K : Type u} {A : Type v} [Field K] [Ring A] [Algebra K A] {x : A} : IsAlgebraic K x ↔ IsIntegral K x

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} [Field K] [Ring A] [Algebra K A] : Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A

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

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

theorem isAlgebraic_of_larger_base {K : Type u_1} (L : Type u_2) {A : Type u_5} [Field K] [Field L] [Ring A] [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] {x : A} (A_alg : IsAlgebraic K x) : IsAlgebraic L x

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} [Field K] [Field L] [Ring A] [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] (A_alg : Algebra.IsAlgebraic K A) : Algebra.IsAlgebraic L 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} [Field K] [Ring A] [Algebra K A] (e : A) [FiniteDimensional K A] : IsAlgebraic K e

theorem Algebra.isAlgebraic_of_finite (K : Type u_1) (A : Type u_5) [Field K] [Ring A] [Algebra K A] [FiniteDimensional K A] : Algebra.IsAlgebraic 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} [Field K] [Field L] [CommRing A] [Algebra K L] [Algebra L A] [Algebra K A] [IsScalarTower K L A] (L_alg : Algebra.IsAlgebraic K L) (A_alg : Algebra.IsAlgebraic L A) : Algebra.IsAlgebraic 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.

theorem Algebra.IsAlgebraic.algHom_bijective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (ha : Algebra.IsAlgebraic K L) (f : L →ₐ[K] L) : Function.Bijective ↑f

theorem AlgHom.bijective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (ϕ : L →ₐ[K] L) : Function.Bijective ↑ϕ

@[simp]

theorem Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (ha : Algebra.IsAlgebraic K L) (ϕ : L →ₐ[K] L) : ↑(MulEquiv.symm (Algebra.IsAlgebraic.algEquivEquivAlgHom K L ha)) ϕ = AlgEquiv.ofBijective ϕ (_ : Function.Bijective ↑ϕ)

@[simp]

theorem Algebra.IsAlgebraic.algEquivEquivAlgHom_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (ha : Algebra.IsAlgebraic K L) (ϕ : L ≃ₐ[K] L) : ↑(Algebra.IsAlgebraic.algEquivEquivAlgHom K L ha) ϕ = ↑ϕ

noncomputable def Algebra.IsAlgebraic.algEquivEquivAlgHom (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (ha : Algebra.IsAlgebraic K L) : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

@[reducible]

noncomputable def algEquivEquivAlgHom (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L)

Bijection between algebra equivalences and algebra homomorphisms

theorem exists_integral_multiple {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] [Algebra R S] {z : S} (hz : IsAlgebraic R z) (inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0) : ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x

theorem IsIntegralClosure.exists_smul_eq_mul {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [CommRing S] {L : Type u_3} [Field L] [Algebra R S] [Algebra S L] [Algebra R L] [IsScalarTower R S L] [IsIntegralClosure S R L] (h : Algebra.IsAlgebraic R L) (inj : Function.Injective ↑(algebraMap R L)) (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} [Field K] [Field L] [Algebra K L] {x : L} {p : Polynomial K} (aeval_ne : ↑(Polynomial.aeval x) (Polynomial.divX p) ≠ 0) : x⁻¹ = ↑(Polynomial.aeval x) (Polynomial.divX p) / (↑(Polynomial.aeval x) p - ↑(algebraMap K L) (Polynomial.coeff p 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 : Polynomial.coeff p 0 ≠ 0) : x⁻¹ = -(↑(Polynomial.aeval x) (Polynomial.divX p) / ↑(algebraMap K L) (Polynomial.coeff p 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 : { x // x ∈ A }} {p : Polynomial K} (aeval_eq : ↑(Polynomial.aeval x) p = 0) (coeff_zero_ne : Polynomial.coeff p 0 ≠ 0) : (↑x)⁻¹ ∈ A

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 : { x // x ∈ A }} (hx : IsAlgebraic K ↑x) : (↑x)⁻¹ ∈ A

theorem Subalgebra.isField_of_algebraic {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (A : Subalgebra K L) (hKL : Algebra.IsAlgebraic K L) : 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 (Polynomial R') (R' → S')

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

See the instance_diamonds test for details.

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

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

See the instance_diamonds test for details.

@[simp]

theorem polynomial_smul_apply (R' : Type u) (S' : Type v) [Semiring R'] [SMul R' S'] (p : Polynomial R') (f : R' → S') (x : R') : (Polynomial R' • (R' → S')) (R' → S') instHSMul p f x = Polynomial.eval x p • f x

@[simp]

theorem polynomial_smul_apply' (R' : Type u) (S' : Type v) (T' : Type w) [CommSemiring R'] [Semiring S'] [Algebra R' S'] [SMul S' T'] (p : Polynomial R') (f : S' → T') (x : S') : (Polynomial R' • (S' → T')) (S' → T') instHSMul p f x = ↑(Polynomial.aeval x) p • f x

noncomputable def Polynomial.algebraPi (R' : Type u) (S' : Type v) (T' : Type w) [CommSemiring R'] [CommSemiring S'] [CommSemiring T'] [Algebra R' S'] [Algebra S' T'] : Algebra (Polynomial R') (S' → T')

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

@[simp]

theorem Polynomial.algebraMap_pi_eq_aeval (R' : Type u) (S' : Type v) (T' : Type w) [CommSemiring R'] [CommSemiring S'] [CommSemiring T'] [Algebra R' S'] [Algebra S' T'] : ↑(algebraMap (Polynomial R') (S' → T')) = fun p z => ↑(algebraMap ((fun x => S') p) T') (↑(Polynomial.aeval z) p)

@[simp]

theorem Polynomial.algebraMap_pi_self_eq_eval (R' : Type u) [CommSemiring R'] : ↑(algebraMap (Polynomial R') (R' → R')) = fun p z => Polynomial.eval z p