The degree of the radical extensions y ^ n = c t ^ a (t - 1) ^ b of k(t) #
Let F = k(t)(y) with y ^ n = c t ^ a (t - 1) ^ b for a nonzero c ∈ k and a, b ∈ ℤ. The
orders of the radicand at the places 0, 1 and ∞ of k(t) are a, b and -(a + b)
(TauCeti.Place.ord_algebraMap_mul_X_zpow_mul_X_sub_one_zpow and its specializations). If n is
coprime to one of them, then X ^ n - c t ^ a (t - 1) ^ b is irreducible over k(t) and
[F : k(t)] = n (Stichtenoth, Corollary 3.7.4; this is
Valuation.finrank_eq_of_pow_eq_of_gcd_ord_eq_one).
Main results #
TauCeti.finrank_eq_of_pow_eq_X_zpow_mul_X_sub_one_zpow: the degree ofy ^ n = c t ^ a (t - 1) ^ boverk(t)isn.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Corollary 3.7.4.
theorem
TauCeti.finrank_eq_of_pow_eq_X_zpow_mul_X_sub_one_zpow
{k : Type u_1}
{F : Type u_2}
[Field k]
[Field F]
[Algebra (RatFunc k) F]
{y : F}
{n : ℕ}
{c : k}
{a b : ℤ}
(hgen : (RatFunc k)⟮y⟯ = ⊤)
(hy : y ^ n = (algebraMap (RatFunc k) F) ((algebraMap k (RatFunc k)) c * RatFunc.X ^ a * (RatFunc.X - 1) ^ b))
(hc : c ≠ 0)
(hcop : (↑n).gcd a = 1 ∨ (↑n).gcd b = 1 ∨ (↑n).gcd (a + b) = 1)
:
The degree of y ^ n = c t ^ a (t - 1) ^ b: if F = k(t)(y) with
y ^ n = c t ^ a (t - 1) ^ b for a nonzero c ∈ k, and n is coprime to one of a, b and
a + b, then [F : k(t)] = n.