Bivariate polynomials and adjoining transcendental elements

Main results

• IsAlgebraic.adjoin_singleton: Given two transcendental elements a, b over R, if one of them, say a, is algebraic over R[b] then b is algebraic over R[a].

noncomputable def Polynomial.Bivariate.Transcendental.algEquivAdjoin {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {x : A} (hx : Transcendental R x) : Polynomial (Polynomial R) ≃ₐ[R] Polynomial ↥(Algebra.adjoin R {x})

The AlgEquiv between R[X][Y] and R[a][Y] for some transcendental a.

Equations

• Polynomial.Bivariate.Transcendental.algEquivAdjoin hx = Polynomial.mapAlgEquiv (Polynomial.algEquivOfTranscendental R x hx)

theorem Polynomial.Bivariate.Transcendental.algEquivAdjoin_apply {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {x : A} (hx : Transcendental R x) (p : Polynomial (Polynomial R)) : (algEquivAdjoin hx) p = (mapAlgHom (aeval ⟨x, ⋯⟩)) p

theorem Polynomial.Bivariate.Transcendental.algEquivAdjoin_swap_eq_aeval {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {x : A} (hx : Transcendental R x) (p : Polynomial (Polynomial R)) : (algEquivAdjoin hx) (swap p) = (aeval (C ⟨x, ⋯⟩)) p

theorem Polynomial.Bivariate.aeval_aeval_eq_aeval_algEquivAdjoin {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} (y : B) (hx : Transcendental R x) (p : Polynomial (Polynomial R)) : (aeval ((algebraMap A B) x)) ((aeval (C ⟨y, ⋯⟩)) p) = (aeval y) ((Transcendental.algEquivAdjoin hx) p)

theorem IsAlgebraic.adjoin_singleton {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_3} [CommRing B] [Algebra A B] [Algebra R B] [IsScalarTower R A B] {x : A} {y : B} (hx : Transcendental R x) (hy : Transcendental R y) (h : IsAlgebraic (↥(Algebra.adjoin R {x})) y) : IsAlgebraic (↥(Algebra.adjoin R {y})) ((algebraMap A B) x)