The Hurwitz bound on a tame automorphism group

Let F / k be an algebraic function field of genus g ≥ 2 with exact constant field k, and let G be a finite group of k-automorphisms of F every place of which is tame over the fixed field F^G. Then

|G| ≤ 84 (g - 1).

The proof is the classical one. The fixed field is a function field over k (TauCeti.IsFunctionField.fixedField) with F / F^G Galois of degree |G| (Artin), so the tame Hurwitz genus formula reads

2g - 2 = |G| (2γ - 2) + deg Diff_tame(F / F^G)

with γ the genus of F^G, and the tame different is the branch data of the extension (TauCeti.Divisor.degree_tameDifferent_eq_finrank_mul_sum):

deg Diff_tame(F / F^G) = |G| ∑_P (1 - 1/e_P) deg P,

the sum over the ramified places P of F^G. Dividing by |G|, the deficit of the branch data (γ; e_P) is (2g - 2)/|G| > 0, so it is at least 1/42 (TauCeti.one_div_forty_two_le_hyperbolic_deficit), which is the bound.

The tameness hypothesis is load-bearing: without it the bound can fail in positive characteristic. It holds automatically in characteristic zero, and over a perfect constant field whenever |G| is prime to the characteristic.

Main results

• TauCeti.natCard_le_eighty_four_mul_genus_sub_one: the Hurwitz bound, |G| ≤ 84 (g - 1) for a finite tame group of automorphisms of a function field of genus at least two.
• TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_not_dvd: the same with no tameness hypothesis, over a perfect constant field, for a group whose order is prime to the characteristic.
• TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_charZero: the same with no tameness hypothesis, over a constant field of characteristic zero, with TauCeti.card_algEquiv_le_eighty_four_mul_genus_sub_one_of_charZero for the full automorphism group once it is finite.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Exercise 3.18.
• G. D. Villa Salvador, Topics in the Theory of Algebraic Function Fields, Birkhäuser, 2006, Chapter 11.

theorem TauCeti.natCard_le_eighty_four_mul_genus_sub_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (G : Subgroup Gal(F/k)) [Finite ↥G] (hgenus : 2 ≤ genus k F) (htame : ∀ (P : Place k F), Place.IsTame k (↥(IntermediateField.fixedField G)) P) : Nat.card ↥G ≤ 84 * (genus k F - 1)

The Hurwitz bound (Stichtenoth, Exercise 3.18): a finite group G of automorphisms of a function field of genus g ≥ 2, every place of which is tame over the fixed field, has order at most 84 (g - 1).

theorem TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_not_dvd {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [PerfectField k] (p : ℕ) [CharP k p] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (G : Subgroup Gal(F/k)) [Finite ↥G] (hgenus : 2 ≤ genus k F) (hp : ¬p ∣ Nat.card ↥G) : Nat.card ↥G ≤ 84 * (genus k F - 1)

The Hurwitz bound for a group of order prime to the characteristic (Stichtenoth, Exercise 3.18): over a perfect constant field of characteristic p, a finite group G of automorphisms of a function field of genus g ≥ 2 with p ∤ |G| has order at most 84 (g - 1).

The ramification index of a place of F over the fixed field divides |G|, by the fundamental identity for the Galois extension F / F^G, so it too is prime to p and every place is tame (TauCeti.Place.isTame_iff_not_dvd_ramificationIdx).

theorem TauCeti.natCard_le_eighty_four_mul_genus_sub_one_of_charZero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [CharZero k] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (G : Subgroup Gal(F/k)) [Finite ↥G] (hgenus : 2 ≤ genus k F) : Nat.card ↥G ≤ 84 * (genus k F - 1)

The Hurwitz bound in characteristic zero (Stichtenoth, Exercise 3.18): a finite group of automorphisms of a function field of genus g ≥ 2 with exact constant field of characteristic zero has order at most 84 (g - 1). No tameness hypothesis is needed: every place is tame (TauCeti.Place.isTame_of_charZero).

theorem TauCeti.card_algEquiv_le_eighty_four_mul_genus_sub_one_of_charZero {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [CharZero k] [Finite Gal(F/k)] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (hgenus : 2 ≤ genus k F) : Nat.card Gal(F/k) ≤ 84 * (genus k F - 1)

The Hurwitz bound for the whole automorphism group: over a constant field of characteristic zero, a function field of genus g ≥ 2 whose automorphism group is finite has |Aut(F / k)| ≤ 84 (g - 1).