Transcendental elements under translations and algebra maps

Adding a base-ring constant to a transcendental element preserves transcendence, over an arbitrary commutative ring and in an arbitrary ring algebra. So does applying an injective algebra homomorphism, the transcendental counterpart of Mathlib's isAlgebraic_algHom_iff. An algebraic extension of scalars without zero divisors also preserves transcendence under an injective algebra map into a common overring, and so does a nonconstant polynomial with coefficients in a field, mapped into an algebra (Transcendental.aeval_map). Dually, every root in A of a polynomial over R is algebraic over R (isAlgebraic_of_mem_aroots). The kernel of an algebra map into a field algebraic over the base field is a maximal ideal (AlgHom.ker_isMaximal_of_isAlgebraic). Every element of a finite-dimensional left ideal of an algebra over a field is algebraic (Submodule.isAlgebraic_of_mem).

theorem isAlgebraic_of_mem_aroots {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [IsDomain A] [Algebra R A] {p : Polynomial R} {x : A} (hx : x ∈ p.aroots A) : IsAlgebraic R x

A root in A of a polynomial over R is algebraic over R.

theorem AlgHom.ker_isMaximal_of_isAlgebraic {F : Type u_1} {A : Type u_2} {E : Type u_3} [Field F] [CommRing A] [Algebra F A] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (ψ : A →ₐ[F] E) : (RingHom.ker ψ).IsMaximal

The kernel of an F-algebra map into a field algebraic over the field F is a maximal ideal, since the image is a field.

theorem Submodule.isAlgebraic_of_mem {K : Type u_1} {B : Type u_2} [Field K] [Ring B] [Algebra K B] (J : Submodule K B) [FiniteDimensional K ↥J] (hJ : ∀ (b : B) {y : B}, y ∈ J → b * y ∈ J) {x : B} (hxJ : x ∈ J) : IsAlgebraic K x

Every element of a finite-dimensional left ideal of an algebra over a field, given as a scalar submodule closed under left multiplication, is algebraic.

theorem Transcendental.add_algebraMap {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {x : A} (hx : Transcendental R x) (c : R) : Transcendental R (x + (algebraMap R A) c)

Translating a transcendental element by a constant keeps it transcendental.

theorem Transcendental.algHom {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {x : A} {B : Type u_3} {G : Type u_4} [Ring B] [Algebra R B] [FunLike G A B] [AlgHomClass G R A B] (f : G) (hf : Function.Injective ⇑f) (hx : Transcendental R x) : Transcendental R (f x)

An injective algebra homomorphism carries a transcendental element to a transcendental element.

theorem Transcendental.algebraMap_of_isAlgebraic {R : Type u_3} {S : Type u_4} {A : Type u_5} {B : Type u_6} [CommRing R] [CommRing S] [NoZeroDivisors S] [CommRing A] [Ring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S B] [Algebra A B] [IsScalarTower R S B] [IsScalarTower R A B] [Algebra.IsAlgebraic R S] [FaithfulSMul A B] {x : A} (hx : Transcendental R x) : Transcendental S ((algebraMap A B) x)

An algebraic extension of scalars without zero divisors preserves transcendence after an injective algebra map into a common overring.

theorem Transcendental.aeval_map {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {x : A} {K : Type u_3} [Field K] [Algebra K R] (hx : Transcendental R x) {q : Polynomial K} (hq : 0 < q.natDegree) : Transcendental R ((Polynomial.aeval x) (Polynomial.map (algebraMap K R) q))

A nonconstant polynomial with coefficients in a field K, mapped into a K-algebra R, carries an element transcendental over R to a transcendental element.