The rational function field as a base for a transcendental element

Let F be an extension of a field k and let x ∈ F be transcendental over k. Mathlib's RatFunc.algEquivOfTranscendental identifies k(X) with the intermediate field k⟮x⟯; composing with its inclusion into F makes F an algebra over k(X) in which X acts as x. This file packages that algebra structure together with the transfers along it of the scalar tower over k and of separability over k⟮x⟯.

The structure is not an instance: it depends on the element x and on a proof, and distinct transcendental elements induce distinct k(X)-algebra structures on the same F. It is meant to be introduced locally with letI.

The nonconstant rational function X - X⁻¹ is also shown to be transcendental. Consequently substitution at it loses no polynomial information, including in positive characteristic.

Main definitions

• TauCeti.ratFuncAlgebraOfTranscendental: the k(X)-algebra structure on F sending X to x.

Main results

• TauCeti.algebraMap_ratFuncAlgebraOfTranscendental_X: the variable X acts as x.
• TauCeti.isScalarTower_ratFuncAlgebraOfTranscendental: the structure extends the given k-algebra structure.
• TauCeti.isSeparable_ratFuncAlgebraOfTranscendental: separability over k⟮x⟯ transfers to separability over k(X).
• TauCeti.transcendental_ratFunc_X_sub_inv: X - X⁻¹ is transcendental.

theorem TauCeti.transcendental_ratFunc_X_sub_inv (k : Type u_1) [Field k] : Transcendental k (RatFunc.X - RatFunc.X⁻¹)

The rational function X - X⁻¹ is transcendental over the coefficient field, in every characteristic.

@[instance_reducible]

noncomputable def TauCeti.ratFuncAlgebraOfTranscendental {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) : Algebra (RatFunc k) F

The RatFunc k-algebra structure on F induced by a transcendental element x, with RatFunc.X acting as x.

Equations

• TauCeti.ratFuncAlgebraOfTranscendental hx = (k⟮x⟯.val.comp ↑(RatFunc.algEquivOfTranscendental x hx)).toAlgebra

theorem TauCeti.algebraMap_ratFuncAlgebraOfTranscendental_apply {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) (r : RatFunc k) : (algebraMap (RatFunc k) F) r = ↑((RatFunc.algEquivOfTranscendental x hx) r)

The structure map of ratFuncAlgebraOfTranscendental hx is the embedding through k(x).

@[simp]

theorem TauCeti.algebraMap_ratFuncAlgebraOfTranscendental_X {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) : (algebraMap (RatFunc k) F) RatFunc.X = x

Under ratFuncAlgebraOfTranscendental hx, the rational-function variable maps to x.

theorem TauCeti.isScalarTower_ratFuncAlgebraOfTranscendental {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) : IsScalarTower k (RatFunc k) F

The RatFunc k-algebra structure induced by x extends the given k-algebra structure.

theorem TauCeti.isSeparable_ratFuncAlgebraOfTranscendental {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : Algebra.IsSeparable (RatFunc k) F

Separability over k(x) transfers to the rational-function algebra structure induced by x.