The deficit of branch data

Branch data is a genus γ together with a multiset of ramification indices e₁, …, e_r, each at least two, and its deficit is

2γ - 2 + ∑ᵢ (1 - 1/eᵢ).

For a quotient of a function field of genus g by a finite tame group of automorphisms G, Riemann--Hurwitz makes the deficit of the branch data of F / F^G equal to (2g - 2)/|G|, so a lower bound on a positive deficit is an upper bound on |G|.

The sharp bound is 1/42, attained by the genus-zero data (2, 3, 7). It is reached only there: each branch point contributes between 1/2 and 1, so genus at least two leaves at least 2 and genus one at least 1/2, while genus zero needs more than two branch points, and with four or more of them a positive deficit is at least 1/6. Only genus-zero data with exactly three branch points comes closer, and there the deficit 1 - 1/a - 1/b - 1/c is the hyperbolic triple bound of TauCeti/Data/Rat/HurwitzTriangle.lean, whose values do drop below 1/6 — (2, 3, 8) gives 1/24 — down to 1/42.

Main results

• TauCeti.one_div_forty_two_le_hyperbolic_deficit: a positive deficit is at least 1/42.
• TauCeti.hyperbolic_deficit_two_three_seven: the genus-zero data (2, 3, 7) attains it.
• TauCeti.half_le_one_sub_one_div and Nat.one_sub_one_div_le_one: the contribution of one branch point, with the sums TauCeti.card_div_two_le_sum_one_sub_one_div, Multiset.sum_one_sub_one_div_le_card and TauCeti.sum_one_sub_one_div_eq_card_div_two.

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Exercise 3.18.

theorem Nat.one_sub_one_div_le_one (n : ℕ) : 1 - 1 / ↑n ≤ 1

The contribution 1 - 1/n of a branch point is at most 1.

theorem Multiset.sum_one_sub_one_div_le_card (e : Multiset ℕ) : (map (fun (n : ℕ) => 1 - 1 / ↑n) e).sum ≤ ↑e.card

The total contribution of the branch points is at most their number.

theorem TauCeti.half_le_one_sub_one_div {n : ℕ} (hn : 2 ≤ n) : 1 / 2 ≤ 1 - 1 / ↑n

The contribution 1 - 1/n of a branch point of index at least two is at least 1/2.

theorem TauCeti.card_div_two_le_sum_one_sub_one_div {e : Multiset ℕ} (he : ∀ n ∈ e, 2 ≤ n) : ↑e.card / 2 ≤ (Multiset.map (fun (n : ℕ) => 1 - 1 / ↑n) e).sum

Half the number of branch points is at most their total contribution.

theorem TauCeti.sum_one_sub_one_div_eq_card_div_two {e : Multiset ℕ} (he : ∀ n ∈ e, n = 2) : (Multiset.map (fun (n : ℕ) => 1 - 1 / ↑n) e).sum = ↑e.card / 2

If every index is two, the total contribution of the branch points is half their number: this is the boundary case, where four branch points in genus zero give deficit zero.

theorem TauCeti.one_div_forty_two_le_hyperbolic_deficit {e : Multiset ℕ} {γ : ℕ} (he : ∀ n ∈ e, 2 ≤ n) (hpos : 0 < 2 * ↑γ - 2 + (Multiset.map (fun (n : ℕ) => 1 - 1 / ↑n) e).sum) : 1 / 42 ≤ 2 * ↑γ - 2 + (Multiset.map (fun (n : ℕ) => 1 - 1 / ↑n) e).sum

The sharp numerical bound for hyperbolic branch data: for a genus γ and ramification indices all at least two, a positive deficit 2γ - 2 + ∑ᵢ (1 - 1/eᵢ) is at least 1/42.

For a function field of genus g and a finite tame group of automorphisms G, Riemann--Hurwitz makes the deficit of the branch data of F / F^G equal to (2g - 2)/|G|, so this is the numerical half of the bound |G| ≤ 84 (g - 1). Outside genus-zero data with exactly three branch points a positive deficit is at least 1/6; the smaller values, down to 1/42 at (2, 3, 7), are the hyperbolic triples.

theorem TauCeti.hyperbolic_deficit_two_three_seven : 2 * ↑0 - 2 + (Multiset.map (fun (n : ℕ) => 1 - 1 / ↑n) {2, 3, 7}).sum = 1 / 42

The genus-zero branch data (2, 3, 7) attains the bound 1/42, so the constant in TauCeti.one_div_forty_two_le_hyperbolic_deficit cannot be improved. Whether a function field and a group of automorphisms realize this datum is a separate question.