The Hurwitz genus formula

Let F' / k' be a finite separable extension of the algebraic function field F / k, with exact constant fields and k' / k finite separable, and write g and g' for the genera of F and F'. The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13) relates the two genera through the degree of the different divisor Diff(F'/F):

[k' : k] · (2g' - 2) = [F' : F] · (2g - 2) + [k' : k] · deg Diff(F'/F).

It is the degree of the divisor identity (Cotr ω) = Con (ω) + Diff(F'/F) (TauCeti.weilDifferentialDivisor_weilDifferentialCotrace) for any nonzero Weil differential ω of F: the divisor of a nonzero Weil differential has degree 2g - 2, and the conorm multiplies degrees by [F' : F] / [k' : k] (TauCeti.Divisor.finrank_mul_degree_conorm). Since k' / k is separable and k is the exact constant field of F, [k' : k] divides [F' : F], and dividing through gives the familiar form

2g' - 2 = n(F'/F) · (2g - 2) + deg Diff(F'/F)

with the geometric degree n(F'/F) = [F' : F k']; when k' = k this is [F' : F].

Main results

• TauCeti.hurwitz_genus_formula: the Hurwitz genus formula, cross-multiplied (Stichtenoth, Theorem 3.4.13).
• TauCeti.hurwitz_genus_formula_geometricDegree: the Hurwitz genus formula through the geometric degree.
• TauCeti.geometricDegree_mul_add_degree_tameDifferent_le and TauCeti.two_mul_genus_sub_two_eq_iff_forall_isTame: the tame lower bound 2g' - 2 ≥ n(F'/F) · (2g - 2) + ∑_{P'} (e(P' ∣ P) - 1) · deg P', with equality exactly when every place of F' is tame (Stichtenoth, Corollary 3.5.6).
• TauCeti.genus_le_genus: g ≤ g' (Stichtenoth, Corollary 3.5.7).
• TauCeti.hurwitz_genus_formula_ratFunc: 2g - 2 = -2 [F : k(x)] + deg Diff(F / k(x)) for a finite separable extension of the rational function field (Stichtenoth, Corollary 3.4.14).
• TauCeti.different_ne_zero_of_one_lt_finrank: a finite separable extension of k(x) of degree greater than one has nonzero different (Stichtenoth, Corollary 3.5.8).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 3.4.13, Corollaries 3.4.14, 3.5.6, 3.5.7 and 3.5.8.

theorem TauCeti.hurwitz_genus_formula {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'] [FiniteDimensional k k'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') : ↑(Module.finrank k k') * (2 * ↑(genus k' F') - 2) = ↑(Module.finrank F F') * (2 * ↑(genus k F) - 2) + ↑(Module.finrank k k') * Divisor.degree (Divisor.different k' F' hF)

The Hurwitz genus formula (Stichtenoth, Theorem 3.4.13): for a finite separable extension F' / k' of the function field F / k, both with exact constants and with k' / k finite separable, [k' : k] · (2g' - 2) = [F' : F] · (2g - 2) + [k' : k] · deg Diff(F'/F).

theorem TauCeti.hurwitz_genus_formula_geometricDegree {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'] [FiniteDimensional k k'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') : 2 * ↑(genus k' F') - 2 = ↑(geometricDegree F k' F') * (2 * ↑(genus k F) - 2) + Divisor.degree (Divisor.different k' F' hF)

The Hurwitz genus formula through the geometric degree (Stichtenoth, Theorem 3.4.13): under the hypotheses of TauCeti.hurwitz_genus_formula, 2g' - 2 = n(F'/F) · (2g - 2) + deg Diff(F'/F), where n(F'/F) = [F' : F k'] is the geometric degree.

theorem TauCeti.geometricDegree_mul_add_degree_tameDifferent_le {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'] [FiniteDimensional k k'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') : ↑(geometricDegree F k' F') * (2 * ↑(genus k F) - 2) + Divisor.degree (Divisor.tameDifferent k' F' hF) ≤ 2 * ↑(genus k' F') - 2

The Hurwitz genus formula, tame lower bound (Stichtenoth, Corollary 3.5.6(a)): under the hypotheses of TauCeti.hurwitz_genus_formula, n(F'/F) · (2g - 2) + ∑_{P'} (e(P' ∣ P) - 1) · deg P' ≤ 2g' - 2, the sum being the degree of the tame different.

theorem TauCeti.two_mul_genus_sub_two_eq_iff_forall_isTame {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'] [FiniteDimensional k k'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') : 2 * ↑(genus k' F') - 2 = ↑(geometricDegree F k' F') * (2 * ↑(genus k F) - 2) + Divisor.degree (Divisor.tameDifferent k' F' hF) ↔ ∀ (P' : Place k' F'), Place.IsTame k F P'

The Hurwitz genus formula, tame case (Stichtenoth, Corollary 3.5.6(b)): under the hypotheses of TauCeti.hurwitz_genus_formula, the tame lower bound 2g' - 2 = n(F'/F) · (2g - 2) + ∑_{P'} (e(P' ∣ P) - 1) · deg P' is an equality exactly when every place of F' is tame over F.

theorem TauCeti.genus_le_genus {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'] [FiniteDimensional k k'] [Algebra.IsSeparable k k'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hex : IsIntegrallyClosedIn k F) (hex' : IsIntegrallyClosedIn k' F') : genus k F ≤ genus k' F'

The genus does not decrease in a finite separable extension (Stichtenoth, Corollary 3.5.7): under the hypotheses of TauCeti.hurwitz_genus_formula, g ≤ g'.

Separable extensions of the rational function field

theorem TauCeti.hurwitz_genus_formula_ratFunc {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F] (hex : IsIntegrallyClosedIn k F) : 2 * ↑(genus k F) - 2 = -2 * ↑(Module.finrank (RatFunc k) F) + Divisor.degree (Divisor.different k F ⋯)

The Hurwitz genus formula over a rational subfield (Stichtenoth, Corollary 3.4.14): for a finite separable extension F of the rational function field k(x) with exact constant field k, 2g - 2 = -2 [F : k(x)] + deg Diff(F / k(x)).

theorem TauCeti.different_ne_zero_of_one_lt_finrank {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] [FiniteDimensional (RatFunc k) F] [Algebra.IsSeparable (RatFunc k) F] (hex : IsIntegrallyClosedIn k F) (h : 1 < Module.finrank (RatFunc k) F) : Divisor.different k F ⋯ ≠ 0

A separable extension of the rational function field of degree greater than one has nonzero different (Stichtenoth, Corollary 3.5.8): if F / k(x) is finite separable of degree > 1 and k is the exact constant field of F, some place of F has positive different exponent over k(x).