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.

Main definitions

• IsAlgebraic: algebraic elements of an algebra.
• Transcendental: transcendental elements of an algebra are those that are not algebraic.
• Subalgebra.IsAlgebraic: a subalgebra is algebraic if all its elements are algebraic.
• Algebra.IsAlgebraic: an algebra is algebraic if all its elements are algebraic.
• Algebra.Transcendental: an algebra is transcendental if some element is transcendental.

Main results

• transcendental_iff: an element x : A is transcendental over R iff out of R[X] only the zero polynomial evaluates to 0 at x.
• Subalgebra.isAlgebraic_iff: a subalgebra is algebraic iff it is algebraic as an algebra.

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 transcendental_iff {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {x : A} : Transcendental R x ↔ ∀ (p : Polynomial R), (Polynomial.aeval x) p = 0 → p = 0

An element x is transcendental over R if and only if for any polynomial p, Polynomial.aeval x p = 0 implies p = 0. This is similar to algebraicIndependent_iff.

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.

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

• isAlgebraic (x : A) : IsAlgebraic R x

class Algebra.Transcendental (R : Type u) (A : Type v) [CommRing R] [Ring A] [Algebra R A] : Prop

An algebra is transcendental if some element is transcendental.

• transcendental : ∃ (x : A), Transcendental R x

theorem Algebra.nontrivial_of_isAlgebraic (R : Type u) (A : Type v) [CommRing R] [Ring A] [Algebra R A] [Algebra.IsAlgebraic R A] : Nontrivial R

theorem Algebra.isAlgebraic_def {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] : Algebra.IsAlgebraic R A ↔ ∀ (x : A), IsAlgebraic R x

theorem Algebra.transcendental_def {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] : Algebra.Transcendental R A ↔ ∃ (x : A), Transcendental R x

theorem Algebra.transcendental_iff_not_isAlgebraic {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] : Algebra.Transcendental R A ↔ ¬Algebra.IsAlgebraic R A

theorem Subalgebra.isAlgebraic_iff {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : S.IsAlgebraic ↔ Algebra.IsAlgebraic R ↥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 ↔ ⊤.IsAlgebraic

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