The different of a radical extension y ^ n = u

Let F' / k' be a finite separable extension of the field extension F / k, generated by an element y with y ^ n = u for some nonzero u ∈ F, where n is invertible in k. At a place P' of F' over the place P of F, write r_P = gcd(n, ord_P u). Stichtenoth's Proposition 3.7.3(b) gives the ramification data e(P' ∣ P) = n / r_P and d(P' ∣ P) = n / r_P - 1. This file proves the two extreme cases, which together cover every place when n is prime. Both rest on Stichtenoth's Theorem 3.5.10(a) applied to X ^ n - c: if F' = F(z) with z ^ n = c regular at P, then d(P' ∣ P) ≤ (n - 1) · ord_{P'} z.

• If n ∣ ord_P u (that is, r_P = n), then P is unramified in F': d(P' ∣ P) = 0 and e(P' ∣ P) = 1.
• If gcd(n, ord_P u) = 1, then d(P' ∣ P) = n - 1.

For n = 2 this is the different of y ^ 2 = f(x) over k(x) in characteristic not two: the places over P ramify exactly when ord_P f is odd, each with different exponent one.

Main results

• TauCeti.Place.differentExponent_le_mul_ord_of_pow_eq: d(P' ∣ P) ≤ (n - 1) · ord_{P'} z for a generator z with z ^ n regular at P.
• TauCeti.Place.differentExponent_eq_zero_of_pow_eq_of_dvd_ord and TauCeti.Place.ramificationIdx_eq_one_of_pow_eq_of_dvd_ord: the unramified case.
• TauCeti.Place.differentExponent_add_one_eq_of_pow_eq_of_gcd_ord_eq_one: the totally ramified case, d(P' ∣ P) + 1 = n.
• TauCeti.Place.differentExponent_eq_of_pow_eq_of_prime and TauCeti.Place.ramificationIdx_eq_of_pow_eq_of_prime: the different exponent and ramification index at every place of a radical extension y ^ n = u with n prime.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 3.7.3 and Theorem 3.5.10.

theorem TauCeti.Place.differentExponent_le_mul_ord_of_pow_eq (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} {z : F'} {n : ℕ} {c : F} (hgen : F⟮z⟯ = ⊤) (hz : z ^ n = (algebraMap F F') c) (hn : ↑n ≠ 0) (hc : c ∈ (restrict k F P').integers) (hz0 : z ≠ 0) : ↑(differentExponent k F P') ≤ (↑n - 1) * P'.ord z

The different exponent above a radical generator (Stichtenoth, Theorem 3.5.10(a) for X ^ n - c): if F' = F(z) with z ^ n = c for some c ∈ F regular at the place P below P', z ≠ 0, and n invertible in k, then d(P' ∣ P) ≤ (n - 1) · ord_{P'} z.

theorem TauCeti.Place.differentExponent_eq_zero_of_pow_eq_of_dvd_ord (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} {y : F'} {n : ℕ} {u : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (hu : u ≠ 0) (hdvd : ↑n ∣ (restrict k F P').ord u) : differentExponent k F P' = 0

A radical extension is unramified where the order of the radicand is divisible by the exponent n (Stichtenoth, Proposition 3.7.3(b) with r_P = n): if F' = F(y) with y ^ n = u for a nonzero u ∈ F, n is invertible in k, and n divides the order of u at the place P below P', then d(P' ∣ P) = 0.

theorem TauCeti.Place.ramificationIdx_eq_one_of_pow_eq_of_dvd_ord (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} {y : F'} {n : ℕ} {u : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (hu : u ≠ 0) (hdvd : ↑n ∣ (restrict k F P').ord u) : ramificationIdx F P' = 1

A radical extension is unramified where the order of the radicand is divisible by the exponent n (Stichtenoth, Proposition 3.7.3(b) with r_P = n): if F' = F(y) with y ^ n = u for a nonzero u ∈ F, n is invertible in k, and n divides the order of u at the place P below P', then e(P' ∣ P) = 1.

theorem TauCeti.Place.differentExponent_add_one_eq_of_pow_eq_of_gcd_ord_eq_one (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} {y : F'} {n : ℕ} {u : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (hu : u ≠ 0) (h : (↑n).gcd ((restrict k F P').ord u) = 1) : differentExponent k F P' + 1 = n

The different exponent of a totally ramified radical extension (Stichtenoth, Proposition 3.7.3(b) with r_P = 1): if F' = F(y) with y ^ n = u for a nonzero u ∈ F, n is invertible in k, and n is coprime to the order of u at the place P below P', then d(P' ∣ P) = n - 1, stated as d(P' ∣ P) + 1 = n so that no truncated subtraction appears.

theorem TauCeti.Place.differentExponent_eq_of_pow_eq_of_prime (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} {y : F'} {n : ℕ} {u : F} (hp : Nat.Prime n) (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (hu : u ≠ 0) : differentExponent k F P' = if ↑n ∣ (restrict k F P').ord u then 0 else n - 1

The different exponent of a radical extension of prime exponent (Stichtenoth, Proposition 3.7.3(b)): if F' = F(y) with y ^ n = u for a nonzero u ∈ F, n is prime and invertible in k, then d(P' ∣ P) is 0 when n divides the order of u at the place P below P', and n - 1 otherwise.

theorem TauCeti.Place.ramificationIdx_eq_of_pow_eq_of_prime (k : Type u) {k' : Type u'} (F : Type v) {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {P' : Place k' F'} {y : F'} {n : ℕ} {u : F} (hp : Nat.Prime n) (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (hu : u ≠ 0) : ramificationIdx F P' = if ↑n ∣ (restrict k F P').ord u then 1 else n

The ramification index of a radical extension of prime exponent (Stichtenoth, Proposition 3.7.3(b)): if F' = F(y) with y ^ n = u for a nonzero u ∈ F, n is prime and invertible in k, then the place P below P' is unramified when n divides ord_P u, and e(P' ∣ P) = n otherwise.