Power subfields of a rational function field

For a field K and an exponent n, this file computes the degree of K(X) over the subfield K(X ^ n), and records that K(X) is purely inseparable over K(X ^ q) when q is the exponential characteristic of K. Transporting the first degree along the identification of K(X) with K⟮x⟯ gives [K(x) : K(x ^ n)] = n for an arbitrary transcendental element x of an extension of K.

Main results

• TauCeti.RatFunc.finrank_adjoin_X_pow: [K(X) : K(X ^ n)] = n.
• TauCeti.RatFunc.isPurelyInseparable_adjoin_X_pow: K(X) / K(X ^ q) is purely inseparable for q the exponential characteristic of K.
• TauCeti.relfinrank_adjoin_pow_adjoin: [K(x) : K(x ^ n)] = n for x transcendental.

Mathematical context

Relative and finite-field Frobenius degree computations use this as the inner degree in the tower K(W) / K(x) / K(x^n).

Provenance

The statement was extracted while porting the finite-field Frobenius tower from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, dev/hasse-weil @ 513e83879e2f). The source proves only the finite-field exponent; the arbitrary field and exponent statement here is new, and follows directly from Mathlib's rational-function degree formula.

@[simp]

theorem TauCeti.RatFunc.finrank_adjoin_X_pow (K : Type u_1) [Field K] (n : ℕ) : Module.finrank (↥K⟮RatFunc.X ^ n⟯) (RatFunc K) = n

[K(X) : K(X ^ n)] = n for any field K and any n. At n = 0 both sides read 0: K⟮1⟯ is K, over which K(X) is infinite-dimensional, and Module.finrank reports 0.

instance TauCeti.RatFunc.isPurelyInseparable_adjoin_X_pow (K : Type u_1) [Field K] (q : ℕ) [ExpChar K q] : IsPurelyInseparable (↥K⟮RatFunc.X ^ q⟯) (RatFunc K)

K(X) is purely inseparable over K(X ^ q) when q is the exponential characteristic of K: it is generated by X, whose q-th power lies in K(X ^ q). In characteristic zero q = 1 and the extension is trivial.

theorem TauCeti.relfinrank_adjoin_pow_adjoin {k : Type u_1} [Field k] {F : Type u_2} [Field F] [Algebra k F] {x : F} (hx : Transcendental k x) (n : ℕ) : k⟮x ^ n⟯.relfinrank k⟮x⟯ = n

[k(x) : k(x ^ n)] = n for an element x transcendental over k. This supplies the power-subfield degree formula for arbitrary transcendental parameters.