The genus formula for radical extensions y ^ n = u

Let F' = F(y) with y ^ n = u for a nonzero u ∈ F, where n is invertible in the constant field k of F. At a place P of F write r_P = gcd(n, ord_P u). Every place P' of F' above P has e(P' ∣ P) = n / r_P and d(P' ∣ P) = n / r_P - 1 (TauCeti.Place.ramificationIdx_eq_of_pow_eq and TauCeti.Place.differentExponent_add_one_eq_of_pow_eq), so the different is a rational multiple of a conorm:

n • Diff(F'/F) = Con (∑_P (n - r_P) P).

The sum runs over any finite set S of places of F outside which n divides ord_P u, for instance the zeros and poles of u; the places outside S contribute nothing because r_P = n there. Taking degrees gives [k' : k] deg Diff(F'/F) = ∑_{P ∈ S} (n - r_P) deg P once [F' : F] = n, and the Hurwitz genus formula turns this into Stichtenoth's closed genus formula

[k' : k] (2g' - 2) = n (2g - 2) + ∑_{P ∈ S} (n - r_P) deg P.

Neither a root of unity in the constants nor the irreducibility of X ^ n - u is assumed: the local data does not need them, and the genus formula only uses the degree [F' : F] = n, which is what the irreducibility of X ^ n - u would supply. The genus formula inherits the hypotheses of the Hurwitz genus formula: the constant fields k of F and k' of F' are exact, and k' / k is separable.

When some place P of F has gcd(n, ord_P u) = 1, the hypotheses on F' are consequences (Stichtenoth, Corollary 3.7.4): X ^ n - u is irreducible, so [F' : F] = n, the extension is separable, and the places above P are totally ramified, so k stays the exact constant field of F'. The genus formula then holds with no hypothesis on F':

2g' - 2 = n (2g - 2) + ∑_{P ∈ S} (n - r_P) deg P.

Over F = k(x) with u = f(x) for a squarefree polynomial f of degree m ≥ 1, every zero of f is such a place, r_P = 1 at the zeros of f, and r_∞ = gcd(n, m) at infinity; since the zeros of f have total degree m, this gives 2g' = (n - 1) (m - 2) + n - gcd(n, m).

When instead F contains a primitive n-th root of unity and u is not a p-th power in F for any prime p ∣ n (Stichtenoth's hypotheses for a Kummer extension, Proposition 3.7.3), the degree [F' : F] = n and separability are consequences (TauCeti.finrank_eq_of_pow_eq_of_adjoin_eq_top), and F' / F is cyclic Galois (TauCeti.isGalois_of_pow_eq_of_adjoin_eq_top, TauCeti.isCyclic_of_pow_eq_of_adjoin_eq_top). No place need be totally ramified, so the constant field of F' can grow, and the genus formula keeps the factor [k' : k].

Main results

• TauCeti.Divisor.nsmul_different_eq_conorm_of_pow_eq: n • Diff(F'/F) = Con (∑ (n - r_P) P).
• TauCeti.Divisor.natCast_mul_finrank_mul_degree_different_of_pow_eq: its degree, n [k' : k] deg Diff(F'/F) = [F' : F] ∑ (n - r_P) deg P.
• TauCeti.genus_formula_of_pow_eq: the genus formula [k' : k] (2g' - 2) = n (2g - 2) + ∑ (n - r_P) deg P.
• TauCeti.isIntegrallyClosedIn_of_pow_eq_of_gcd_ord_eq_one: a place with gcd(n, ord_P u) = 1 keeps the constant field exact.
• TauCeti.genus_formula_of_pow_eq_of_isPrimitiveRoot: the genus formula of a Kummer extension, with [F' : F] = n derived from a primitive n-th root of unity in F and the nondegeneracy of u.
• TauCeti.two_mul_genus_sub_two_eq_of_pow_eq_of_gcd_ord_eq_one: the genus formula 2g' - 2 = n (2g - 2) + ∑ (n - r_P) deg P in that case, and TauCeti.two_mul_genus_eq_of_pow_eq_of_gcd_ord_eq_one_ratFunc its form over k(x).
• TauCeti.two_mul_genus_eq_of_pow_eq_of_squarefree: the genus of a superelliptic equation y ^ n = f(x) with f squarefree of degree m, 2g = (n - 1) (m - 2) + n - gcd(n, m).

References

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

The divisor, degree and Hurwitz assembly follows the Artin–Schreier genus formula in TauCeti.FieldTheory.FunctionField.ArtinSchreier.Genus.

theorem TauCeti.Divisor.nsmul_different_eq_conorm_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'] (hF : IsFunctionField k F) {y : F'} {n : ℕ} {u : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (S : Finset (Place k F)) (hS : ∀ P ∉ S, ↑n ∣ P.ord u) : n • different k' F' hF = (conorm k' F') (AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity S fun (P : Place k F) => n - (↑n).gcd (P.ord u))

The different of a radical extension (Stichtenoth, Proposition 3.7.3(b)): for F' = F(y) with y ^ n = u, the different multiplied by n is the conorm of the divisor ∑_{P ∈ S} (n - r_P) P, where r_P = gcd(n, ord_P u) and S is any finite set of places outside which n divides ord_P u.

theorem TauCeti.Divisor.natCast_mul_finrank_mul_degree_different_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'] (hF : IsFunctionField k F) {y : F'} {n : ℕ} {u : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (S : Finset (Place k F)) (hS : ∀ P ∉ S, ↑n ∣ P.ord u) (hF' : IsFunctionField k' F') : ↑n * (↑(Module.finrank k k') * degree (different k' F' hF)) = ↑(Module.finrank F F') * ∑ P ∈ S, (↑n - ↑((↑n).gcd (P.ord u))) * ↑P.degree

The degree of the different of a radical extension, cross-multiplied: for F' = F(y) with y ^ n = u, n · [k' : k] · deg Diff(F'/F) = [F' : F] · ∑_{P ∈ S} (n - r_P) deg P, where r_P = gcd(n, ord_P u) and S is any finite set of places outside which n divides ord_P u. When [F' : F] = n the factor n cancels; see TauCeti.genus_formula_of_pow_eq.

theorem TauCeti.genus_formula_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'] (hF : IsFunctionField k F) {y : F'} {n : ℕ} {u : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (S : Finset (Place k F)) (hS : ∀ P ∉ S, ↑n ∣ P.ord u) [Algebra.IsSeparable k k'] (hF' : IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') (hfin : Module.finrank F F' = n) : ↑(Module.finrank k k') * (2 * ↑(genus k' F') - 2) = ↑n * (2 * ↑(genus k F) - 2) + ∑ P ∈ S, (↑n - ↑((↑n).gcd (P.ord u))) * ↑P.degree

The genus formula for radical extensions (Stichtenoth, Proposition 3.7.3(b) with Theorem 3.4.13): for F' = F(y) of degree n over F with y ^ n = u, n invertible in k, exact constant fields k of F and k' of F', and k' / k separable, [k' : k] (2g' - 2) = n (2g - 2) + ∑_{P ∈ S} (n - r_P) deg P, where r_P = gcd(n, ord_P u) and S is any finite set of places outside which n divides ord_P u.

Kummer extensions

theorem TauCeti.genus_formula_of_pow_eq_of_isPrimitiveRoot {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'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') {y : F'} {n : ℕ} {u : F} (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) {ζ : F} (hζ : IsPrimitiveRoot ζ n) (hu : u ≠ 0) (hnd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (w : F), w ^ p ≠ u) (S : Finset (Place k F)) (hS : ∀ P ∉ S, ↑n ∣ P.ord u) : ↑(Module.finrank k k') * (2 * ↑(genus k' F') - 2) = ↑n * (2 * ↑(genus k F) - 2) + ∑ P ∈ S, (↑n - ↑((↑n).gcd (P.ord u))) * ↑P.degree

The genus formula for Kummer extensions (Stichtenoth, Proposition 3.7.3): let F' = F(y) with y ^ n = u for a nonzero u ∈ F, where F contains a primitive n-th root of unity and u is not a p-th power in F for any prime p ∣ n. If the constant fields k of F and k' of F' are exact and k' / k is separable, then

[k' : k] (2g' - 2) = n (2g - 2) + ∑_{P ∈ S} (n - r_P) deg P,

where r_P = gcd(n, ord_P u) and S is any finite set of places outside which n divides ord_P u. The degree [F' : F] = n and the separability of F' / F are consequences of the hypotheses.

Kummer extensions with a place of coprime order

theorem TauCeti.isIntegrallyClosedIn_of_pow_eq_of_gcd_ord_eq_one {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] {y : F'} {n : ℕ} {u : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (hu : u ≠ 0) (P : Place k F) (hP : (↑n).gcd (P.ord u) = 1) : IsIntegrallyClosedIn k F'

A Kummer extension with a place of coprime order acquires no new constants (Stichtenoth, Corollary 3.7.4): if F' = F(y) with y ^ n = u for a nonzero u ∈ F, n is invertible in the exact constant field k of F, and gcd(n, ord_P u) = 1 at some place P of F, then k is also the exact constant field of F'.

theorem TauCeti.two_mul_genus_sub_two_eq_of_pow_eq_of_gcd_ord_eq_one {k : Type u} {F : Type v} {F' : Type v'} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] {y : F'} {n : ℕ} {u : F} (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hgen : F⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap F F') u) (hn : ↑n ≠ 0) (hu : u ≠ 0) (S : Finset (Place k F)) (hS : ∀ Q ∉ S, ↑n ∣ Q.ord u) (P : Place k F) (hP : (↑n).gcd (P.ord u) = 1) : 2 * ↑(genus k F') - 2 = ↑n * (2 * ↑(genus k F) - 2) + ∑ Q ∈ S, (↑n - ↑((↑n).gcd (Q.ord u))) * ↑Q.degree

The genus formula for Kummer extensions (Stichtenoth, Corollary 3.7.4): let F' = F(y) with y ^ n = u for a nonzero u ∈ F, where n is invertible in the exact constant field k of F, and suppose gcd(n, ord_P u) = 1 at some place P of F. Then

2g' - 2 = n (2g - 2) + ∑_{Q ∈ S} (n - r_Q) deg Q,

where r_Q = gcd(n, ord_Q u) and S is any finite set of places outside which n divides ord_Q u. The degree [F' : F] = n, separability, and exactness of the constants of F' all follow from the place P. No root of unity in k is needed.

theorem TauCeti.two_mul_genus_eq_of_pow_eq_of_gcd_ord_eq_one_ratFunc {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] {y : F} {n : ℕ} {u : RatFunc k} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap (RatFunc k) F) u) (hn : ↑n ≠ 0) (hu : u ≠ 0) (S : Finset (Place k (RatFunc k))) (hS : ∀ Q ∉ S, ↑n ∣ Q.ord u) (P : Place k (RatFunc k)) (hP : (↑n).gcd (P.ord u) = 1) : 2 * ↑(genus k F) = ∑ Q ∈ S, (↑n - ↑((↑n).gcd (Q.ord u))) * ↑Q.degree - 2 * (↑n - 1)

The genus formula for Kummer extensions of k(x): if F = k(x)(y) with y ^ n = u for a nonzero u ∈ k(x), n is invertible in k, and gcd(n, ord_P u) = 1 at some place P of k(x), then

2g = ∑_{Q ∈ S} (n - r_Q) deg Q - 2 (n - 1),

where r_Q = gcd(n, ord_Q u) and S is any finite set of places of k(x) outside which n divides ord_Q u.

theorem TauCeti.two_mul_genus_eq_of_pow_eq_of_squarefree {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] {y : F} {n : ℕ} {f : Polynomial k} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ n = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) (hn : ↑n ≠ 0) (hf : Squarefree f) (hdeg : 0 < f.natDegree) : 2 * ↑(genus k F) = (↑n - 1) * (↑f.natDegree - 2) + ↑n - ↑(n.gcd f.natDegree)

The genus of a superelliptic equation y ^ n = f(x) (Stichtenoth, Corollary 3.7.4 and Example 3.7.6): if F = k(x)(y) with y ^ n = f(x) for a squarefree polynomial f ∈ k[X] of degree m ≥ 1, and n is invertible in k, then

2g = (n - 1) (m - 2) + n - gcd(n, m).

The only places of k(x) over which F can ramify are the zeros of f, each with ramification index n, and the place at infinity, with ramification index n / gcd(n, m); such a place is ramified precisely when its index exceeds 1. Neither a root of unity in k nor any other hypothesis on k is needed.