Hurwitz class numbers

The Hurwitz class number H D of a natural number D counts the positive-definite integral binary quadratic forms a x² + b x y + c y² of discriminant b² - 4 a c = -D up to SL₂(ℤ)-equivalence, where the classes of the multiples of x² + y² count with weight 1/2 and those of the multiples of x² + x y + y² with weight 1/3, and where H 0 = -1/12. These are the class numbers that enter the Eichler–Selberg trace formula for the Hecke operators on S_k(SL₂(ℤ)).

Here H D is defined combinatorially, as a weighted count of the reduced forms TauCeti.reducedForms D of TauCeti.NumberTheory.BinaryQuadraticForm.Reduced: those with |b| ≤ a ≤ c, and with 0 ≤ b whenever |b| = a or a = c. Every positive-definite form is equivalent to exactly one reduced form, so the count is the class count; that comparison is separate. The definition involves no class groups, and it is a finite, decidable sum.

Main definitions

• TauCeti.reducedFormWeight f: the weight 1/2, 1/3 or 1 with which a reduced form counts.
• TauCeti.hurwitzClassNumber D: the Hurwitz class number H D.

Main results

• TauCeti.hurwitzClassNumber_eq_zero_of_mod_four_eq_one_or_two: H D = 0 when D ≡ 1, 2 (mod 4), since a discriminant b² - 4 a c is 0 or 1 modulo 4 (Int.discrim_emod_four).
• The first values H 3 = 1/3, H 4 = 1/2, H 7 = 1, H 8 = 1, H 12 = 4/3, H 15 = 2 and H 16 = 3/2; H 12 and H 16 exercise the two weights on non-primitive forms.

References

• D. Zagier, Nombres de classes et formes modulaires de poids 3/2, C. R. Acad. Sci. Paris Sér. A-B 281 (1975).
• H. Cohen, A Course in Computational Algebraic Number Theory, GTM 138, §5.3.
• A. Popa and D. Zagier, An elementary proof of the Eichler–Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105–122, arXiv:1711.00327.

def TauCeti.reducedFormWeight (f : BinaryQuadraticForm ℤ) : ℚ

The weight with which a reduced form f = a x² + b x y + c y² counts in the Hurwitz class number: 1/2 for the multiples ⟨a, 0, a⟩ of x² + y², 1/3 for the nonzero multiples ⟨a, a, a⟩ of x² + x y + y², and 1 for every other form.

@[simp]

theorem TauCeti.reducedFormWeight_self_zero_self (a : ℤ) : reducedFormWeight { a := a, b := 0, c := a } = 1 / 2

The multiples ⟨a, 0, a⟩ of x² + y² count 1/2.

@[simp]

theorem TauCeti.reducedFormWeight_self_self_self {a : ℤ} (ha : a ≠ 0) : reducedFormWeight { a := a, b := a, c := a } = 1 / 3

The nonzero multiples ⟨a, a, a⟩ of x² + x y + y² count 1/3.

@[simp]

theorem TauCeti.reducedFormWeight_eq_one {f : BinaryQuadraticForm ℤ} (h₁ : ¬(f.b = 0 ∧ f.a = f.c)) (h₂ : ¬(f.a = f.b ∧ f.b = f.c)) : reducedFormWeight f = 1

Every form other than the multiples ⟨a, 0, a⟩ of x² + y² and ⟨a, a, a⟩ of x² + x y + y² counts 1.

@[simp]

theorem TauCeti.reducedFormWeight_smul {r : ℤ} (hr : r ≠ 0) (f : BinaryQuadraticForm ℤ) : reducedFormWeight (r • f) = reducedFormWeight f

Scaling by a nonzero integer does not change the weight of a form.

def TauCeti.hurwitzClassNumber (D : ℕ) : ℚ

The Hurwitz class number H D: H 0 = -1/12, and for D ≠ 0 the number of reduced forms of discriminant -D, primitive or not, each counted with its reducedFormWeight.

The value H 0 = -1/12 is Zagier's normalisation, the one in which the t² = 4 n terms of the Eichler–Selberg trace formula absorb the contribution of the scalar matrices. H D vanishes for D ≡ 1, 2 (mod 4) (hurwitzClassNumber_eq_zero_of_mod_four_eq_one_or_two).

@[simp]

theorem TauCeti.hurwitzClassNumber_zero : hurwitzClassNumber 0 = -1 / 12

H 0 = -1/12 is Zagier's normalisation, not a weighted count of reduced forms as H D is for D ≠ 0 (hurwitzClassNumber_of_ne_zero).

theorem TauCeti.hurwitzClassNumber_of_ne_zero {D : ℕ} (hD : D ≠ 0) : hurwitzClassNumber D = ∑ f ∈ reducedForms D, reducedFormWeight f

H D for D ≠ 0 is the weighted count of the reduced forms of discriminant -D.

@[simp]

theorem TauCeti.hurwitzClassNumber_eq_zero_of_mod_four_eq_one_or_two {D : ℕ} (hD : D % 4 = 1 ∨ D % 4 = 2) : hurwitzClassNumber D = 0

The Hurwitz class number H D is 0 for D ≡ 1, 2 (mod 4).

The first values

@[simp]

theorem TauCeti.hurwitzClassNumber_three : hurwitzClassNumber 3 = 1 / 3

H 3 = 1/3: the only reduced form of discriminant -3 is x² + x y + y², which counts 1/3.

@[simp]

theorem TauCeti.hurwitzClassNumber_four : hurwitzClassNumber 4 = 1 / 2

H 4 = 1/2: the only reduced form of discriminant -4 is x² + y², which counts 1/2.

@[simp]

theorem TauCeti.hurwitzClassNumber_seven : hurwitzClassNumber 7 = 1

H 7 = 1: the only reduced form of discriminant -7 is x² + x y + 2 y².

@[simp]

theorem TauCeti.hurwitzClassNumber_eight : hurwitzClassNumber 8 = 1

H 8 = 1: the only reduced form of discriminant -8 is x² + 2 y².

@[simp]

theorem TauCeti.hurwitzClassNumber_twelve : hurwitzClassNumber 12 = 4 / 3

H 12 = 4/3: the reduced forms of discriminant -12 are x² + 3 y² and the non-primitive 2 (x² + x y + y²), which counts 1/3.

@[simp]

theorem TauCeti.hurwitzClassNumber_fifteen : hurwitzClassNumber 15 = 2

H 15 = 2: the reduced forms of discriminant -15 are x² + x y + 4 y² and 2 x² + x y + 2 y².

@[simp]

theorem TauCeti.hurwitzClassNumber_sixteen : hurwitzClassNumber 16 = 3 / 2

H 16 = 3/2: the reduced forms of discriminant -16 are x² + 4 y² and the non-primitive 2 (x² + y²), which counts 1/2.