Simple transcendental field extensions

A simple transcendental field extension has transcendence degree one.

Combined with the tower rule for linear independence, a family that is linearly independent over the simple extension k⟮x⟯ stays linearly independent over k after multiplying by arbitrary powers of a transcendental element x.

The finite-power statement is the source of dimension growth in the theory of algebraic function fields: multiplying a basis of F / k⟮x⟯ by the powers 1, x, …, xⁿ exhibits (n + 1) [F : k(x)] functions that are independent over k and whose poles are controlled by those of x.

Main results

• Transcendental.trdeg_adjoin_eq_one: the field generated by one transcendental element has transcendence degree one.
• Transcendental.linearIndependent_mul_pow: a k⟮x⟯-linearly independent family in F, multiplied by the powers of a transcendental x, is k-linearly independent.
• Transcendental.linearIndependent_mul_pow_fin: the finite-power restriction used in dimension estimates.

theorem Transcendental.trdeg_adjoin_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) : Algebra.trdeg k ↥k⟮x⟯ = 1

The simple field generated by a transcendental element has transcendence degree one.

theorem Transcendental.linearIndependent_mul_pow {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) {ι : Type u_3} {c : ι → F} (hc : LinearIndependent (↥k⟮x⟯) c) : LinearIndependent k fun (p : ι × ℕ) => c p.1 * x ^ p.2

The growth family: multiplying a k⟮x⟯-linearly independent family by the powers of a transcendental element x yields a k-linearly independent family. This is Mathlib's tower rule linearIndependent_smul, applied to the powers of x inside k⟮x⟯.

theorem Transcendental.linearIndependent_mul_pow_fin {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) {ι : Type u_3} {c : ι → F} (hc : LinearIndependent (↥k⟮x⟯) c) (n : ℕ) : LinearIndependent k fun (p : ι × Fin n) => c p.1 * x ^ ↑p.2

Restrict the growth family to the first n powers of x.