Reduced binary quadratic forms

An integral binary quadratic form a x² + b x y + c y² is reduced when |b| ≤ a ≤ c, and 0 ≤ b whenever |b| = a or a = c (Cohen, Definition 5.3.2). Every positive-definite form is SL₂(ℤ)-equivalent to exactly one reduced form, the boundary conditions being what removes the double count on the edges of the fundamental domain. This file defines the predicate and, for D ≠ 0, the finite set of reduced forms of discriminant -D: a reduced form of discriminant -D < 0 has |b| ≤ a ≤ √(D / 3) and c ≤ D / 3, so the set is a filter of an explicit box and is decidable. Weighted, it counts the Hurwitz class number TauCeti.hurwitzClassNumber.

Main definitions

• TauCeti.IsReducedForm f: the form f = a x² + b x y + c y² is reduced.
• TauCeti.reducedForms D: for D ≠ 0, the finite set of reduced forms of discriminant -D.

Main results

• TauCeti.mem_reducedForms: for D ≠ 0, f ∈ reducedForms D exactly when f.discrim = -D and f is reduced, so the box the definition searches is no restriction.
• TauCeti.a_pos_of_mem_reducedForms, TauCeti.mk_neg_mem_reducedForms: a reduced form of discriminant -D has 0 < a, and ⟨a, -b, c⟩ is reduced along with ⟨a, b, c⟩ when |b| < a < c.
• TauCeti.reducedForms_eq_empty_of_mod_four_eq_one_or_two: there are no reduced forms of discriminant -D when D ≡ 1, 2 (mod 4), since a discriminant b² - 4 a c is 0 or 1 modulo 4 (Int.discrim_emod_four).

Implementation notes

The definitions are exposed, so that the kernel can evaluate reducedForms D, as decide does for the values of TauCeti.hurwitzClassNumber.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, GTM 138, §5.3.

def TauCeti.IsReducedForm (f : BinaryQuadraticForm ℤ) : Prop

The integral binary quadratic form f = a x² + b x y + c y² is reduced: |b| ≤ a ≤ c, and 0 ≤ b whenever |b| = a or a = c (Cohen, Definition 5.3.2).

For a positive-definite form this picks exactly one representative of each SL₂(ℤ)-class: the inequalities place the root τ = (-b + i √(4 a c - b²)) / (2 a) of a τ² + b τ + c in ModularGroup.fd, and the sign condition chooses one of each pair of boundary points that SL₂(ℤ) identifies. Definiteness is not part of the predicate (IsReducedForm ⟨0, 0, 1⟩ holds), but a reduced form with f.discrim < 0 has 0 < f.a (pos_of_nonneg_of_discrim_lt_zero).

@[instance_reducible]

instance TauCeti.instDecidableIsReducedForm (f : BinaryQuadraticForm ℤ) : Decidable (IsReducedForm f)

theorem TauCeti.isReducedForm_iff {f : BinaryQuadraticForm ℤ} : IsReducedForm f ↔ |f.b| ≤ f.a ∧ f.a ≤ f.c ∧ (|f.b| = f.a ∨ f.a = f.c → 0 ≤ f.b)

The form f = a x² + b x y + c y² is reduced exactly when |b| ≤ a ≤ c, and 0 ≤ b whenever |b| = a or a = c.

@[simp]

theorem TauCeti.isReducedForm_smul_iff {r : ℤ} (hr : 0 < r) {f : BinaryQuadraticForm ℤ} : IsReducedForm (r • f) ↔ IsReducedForm f

Scaling by a positive integer preserves and reflects reducedness: r • f is reduced exactly when f is.

def TauCeti.reducedForms (D : ℕ) : Finset (BinaryQuadraticForm ℤ)

The reduced forms a x² + b x y + c y² of discriminant b² - 4 a c = -D.

The definition searches the box 1 ≤ a ≤ √(D / 3), |b| ≤ √(D / 3), 1 ≤ c ≤ D / 3 (with Nat.sqrt), which makes it a finite, decidable set; mem_reducedForms shows that for D ≠ 0 this box loses nothing. For D = 0 the box is empty, so reducedForms 0 = ∅, although every c y² with 0 ≤ c is a reduced form of discriminant 0.

@[simp]

theorem TauCeti.mem_reducedForms {D : ℕ} (hD : D ≠ 0) {f : BinaryQuadraticForm ℤ} : f ∈ reducedForms D ↔ f.discrim = -↑D ∧ IsReducedForm f

The reduced forms of discriminant -D: for D ≠ 0, f ∈ reducedForms D exactly when f.discrim = -D and f is reduced, so the box that reducedForms searches loses nothing.

@[simp]

theorem TauCeti.reducedForms_zero : reducedForms 0 = ∅

The search box of reducedForms 0 is empty.

theorem TauCeti.a_pos_of_mem_reducedForms {D : ℕ} {f : BinaryQuadraticForm ℤ} (hf : f ∈ reducedForms D) : 0 < f.a

A reduced form of discriminant -D has positive first coefficient.

theorem TauCeti.mk_neg_mem_reducedForms {D : ℕ} {f : BinaryQuadraticForm ℤ} (hf : f ∈ reducedForms D) (hba : |f.b| < f.a) (hac : f.a < f.c) : { a := f.a, b := -f.b, c := f.c } ∈ reducedForms D

Changing the sign of the middle coefficient of a reduced form ⟨a, b, c⟩ with |b| < a < c gives a reduced form ⟨a, -b, c⟩ of the same discriminant.

@[simp]

theorem TauCeti.reducedForms_eq_empty_of_mod_four_eq_one_or_two {D : ℕ} (hD : D % 4 = 1 ∨ D % 4 = 2) : reducedForms D = ∅

There are no reduced forms of discriminant -D when D ≡ 1, 2 (mod 4): a discriminant b² - 4 a c is 0 or 1 modulo 4 (Int.discrim_emod_four).