Binary quadratic forms

DefinitionReal quadratic form of an integer coefficient triple#✓fully proved

For integers \(a, b, c\), this is the quadratic form on the real vector space \(\mathbb{R}^2\) given by \((x, y) \mapsto a x^2 + b x y + c y^2\).

def ofCoefficients (q : ℤ × ℤ × ℤ) : QuadraticForm ℝ (ℝ × ℝ) :=
  (q.1 : ℝ) • QuadraticMap.linMulLin (LinearMap.fst ℝ ℝ ℝ) (LinearMap.fst ℝ ℝ ℝ) +
  (q.2.1 : ℝ) • QuadraticMap.linMulLin (LinearMap.fst ℝ ℝ ℝ) (LinearMap.snd ℝ ℝ ℝ) +
  (q.2.2 : ℝ) • QuadraticMap.linMulLin (LinearMap.snd ℝ ℝ ℝ) (LinearMap.snd ℝ ℝ ℝ)

Used by 2

Used byEvaluation of the real quadratic form of a coefficient triple · Positive definiteness for negative discriminant

TheoremEvaluation of the real quadratic form of a coefficient triple#✓fully proved

For integers \(a, b, c\) and real numbers \(x, y\), the real quadratic form of the triple \((a, b, c)\) takes the value \(a x^2 + b x y + c y^2\) at the point \((x, y)\).

theorem ofCoefficients_apply (q : ℤ × ℤ × ℤ) (x y : ℝ) :
    ofCoefficients q (x, y) = (q.1 : ℝ) * x ^ 2 + (q.2.1 : ℝ) * x * y +
      (q.2.2 : ℝ) * y ^ 2

Uses 1 · Used by 1

Statement usesReal quadratic form of an integer coefficient triple

Used byPositive definiteness for negative discriminant

TheoremPositive definiteness for negative discriminant#✓fully proved

Let \(D\) be a positive integer and let \(a, b, c\) be integers with \(a > 0\) and \(b^2 - 4ac = -D\). Then the real quadratic form \((x, y) \mapsto a x^2 + b x y + c y^2\) on \(\mathbb{R}^2\) is positive definite.

theorem ofCoefficients_posDef (D : ℕ) (hD : 0 < D) (q : ℤ × ℤ × ℤ)
    (ha : 0 < q.1) (hd : discrim q.1 q.2.1 q.2.2 = -(D : ℤ)) :
    (ofCoefficients q).PosDef

Uses 2

Statement usesReal quadratic form of an integer coefficient triple

Proof usesEvaluation of the real quadratic form of a coefficient triple

DefinitionThe imaginary square root of \(-D\)#✓fully proved

For a natural number \(D\), the imaginary root of \(D\) is the complex number \(i\sqrt{D}\), where \(\sqrt{D}\) is the nonnegative real square root; it is the square root of \(-D\) with nonnegative imaginary part.

def imaginaryRoot (D : ℕ) : ℂ :=
  Complex.I * (Real.sqrt (D : ℝ) : ℂ)

Used by 9

Used byIdeal class of a binary quadratic form · The form generator is an algebraic integer · Ideal of a binary quadratic form · The ideal of a form is nonzero · The imaginary quadratic field \(\mathbb{Q}(\sqrt{-D})\) · \(\mathbb{Q}(\sqrt{-D})\) is a quadratic extension · The imaginary root is integral over \(\mathbb{Q}\) · The imaginary root is not rational · The imaginary root squares to \(-D\)

TheoremThe imaginary root squares to \(-D\)#✓fully proved

For every natural number \(D\), the complex number \(i\sqrt{D}\) satisfies \((i\sqrt{D})^2 = -D\).

theorem imaginaryRoot_sq (D : ℕ) : imaginaryRoot D ^ 2 = -(D : ℂ)

Uses 1 · Used by 3

Statement usesThe imaginary square root of \(-D\)

Used byThe form generator is an algebraic integer · \(\mathbb{Q}(\sqrt{-D})\) is a quadratic extension · The imaginary root is integral over \(\mathbb{Q}\)

TheoremThe imaginary root is integral over \(\mathbb{Q}\)#✓fully proved

For every natural number \(D\), the complex number \(i\sqrt{D}\) is integral over \(\mathbb{Q}\).

theorem imaginaryRoot_isIntegral (D : ℕ) : IsIntegral ℚ (imaginaryRoot D)

Uses 2 · Used by 4

Statement usesThe imaginary square root of \(-D\)

Proof usesThe imaginary root squares to \(-D\)

Used byIdeal class of a binary quadratic form · Ideal of a binary quadratic form · The ideal of a form is nonzero · \(\mathbb{Q}(\sqrt{-D})\) is a quadratic extension

TheoremThe imaginary root is not rational#✓fully proved

For every positive integer \(D\), the complex number \(i\sqrt{D}\) does not lie in the subfield \(\mathbb{Q}\) of \(\mathbb{C}\).

theorem imaginaryRoot_not_mem_bot (D : ℕ) (hD : 0 < D) :
    imaginaryRoot D ∉ (⊥ : IntermediateField ℚ ℂ)

Uses 1 · Used by 1

Statement usesThe imaginary square root of \(-D\)

Used by\(\mathbb{Q}(\sqrt{-D})\) is a quadratic extension

AbbreviationThe imaginary quadratic field \(\mathbb{Q}(\sqrt{-D})\)#✓fully proved

For a natural number \(D\), this is the subfield \(\mathbb{Q}(i\sqrt{D})\) of \(\mathbb{C}\) generated over \(\mathbb{Q}\) by the imaginary root \(i\sqrt{D}\).

When \(D = 0\) this field is \(\mathbb{Q}\) itself.

abbrev imaginaryQuadraticField (D : ℕ) := ℚ⟮imaginaryRoot D⟯

Uses 1 · Used by 5

Statement usesThe imaginary square root of \(-D\)

Used byIdeal class of a binary quadratic form · The form generator is an algebraic integer · Ideal of a binary quadratic form · The ideal of a form is nonzero · \(\mathbb{Q}(\sqrt{-D})\) is a quadratic extension

Theorem\(\mathbb{Q}(\sqrt{-D})\) is a quadratic extension#✓fully proved

For every positive integer \(D\), the subfield \(\mathbb{Q}(i\sqrt{D})\) of \(\mathbb{C}\) has degree \(2\) over \(\mathbb{Q}\).

theorem imaginaryQuadraticField_finrank (D : ℕ) (hD : 0 < D) :
    Module.finrank ℚ (imaginaryQuadraticField D) = 2

Uses 5

Statement usesThe imaginary quadratic field \(\mathbb{Q}(\sqrt{-D})\)

Proof usesThe imaginary square root of \(-D\) · The imaginary root is integral over \(\mathbb{Q}\) · The imaginary root is not rational · The imaginary root squares to \(-D\)

TheoremThe form generator is an algebraic integer#✓fully proved

Let \(D\) be a natural number and let \(a, b, c\) be integers with \(b^2 - 4ac = -D\). Then the element \((b + i\sqrt{D})/2\) of the field \(\mathbb{Q}(i\sqrt{D}) \subseteq \mathbb{C}\) is integral over \(\mathbb{Z}\).

theorem formGenerator_isIntegral (D : ℕ) (q : ℤ × ℤ × ℤ)
    (hd : discrim q.1 q.2.1 q.2.2 = -(D : ℤ)) :
    IsIntegral ℤ (((q.2.1 : imaginaryQuadraticField D) +
      IntermediateField.AdjoinSimple.gen ℚ (imaginaryRoot D)) / 2)

Uses 3

Statement usesThe imaginary quadratic field \(\mathbb{Q}(\sqrt{-D})\) · The imaginary square root of \(-D\)

Proof usesThe imaginary root squares to \(-D\)

DefinitionIdeal of a binary quadratic form#✓fully proved

Let \(D\) be a natural number, let \(K = \mathbb{Q}(i\sqrt{D}) \subseteq \mathbb{C}\) and let \(\mathcal{O}_K\) be its ring of integers. For integers \(a, b, c\), the ideal of the triple \((a, b, c)\) is the fractional ideal of \(\mathcal{O}_K\) in \(K\) generated by \(a\) and \((b + i\sqrt{D})/2\).

When \(b^2 - 4ac = -D\), the second generator is an algebraic integer.

def formIdeal (D : ℕ) (q : ℤ × ℤ × ℤ) :
    FractionalIdeal (𝓞 (imaginaryQuadraticField D))⁰ (imaginaryQuadraticField D) :=
  FractionalIdeal.spanFinset (𝓞 (imaginaryQuadraticField D)) Finset.univ
    (fun i : Fin 2 => if i = 0 then (q.1 : imaginaryQuadraticField D)
      else ((q.2.1 : imaginaryQuadraticField D) +
        IntermediateField.AdjoinSimple.gen ℚ (imaginaryRoot D)) / 2)

Uses 3 · Used by 2

Statement usesThe imaginary quadratic field \(\mathbb{Q}(\sqrt{-D})\) · The imaginary square root of \(-D\) · The imaginary root is integral over \(\mathbb{Q}\)

Used byIdeal class of a binary quadratic form · The ideal of a form is nonzero

TheoremThe ideal of a form is nonzero#✓fully proved

Let \(D\) be a natural number and let \(a, b, c\) be integers with \(a \ne 0\). Then the fractional ideal of the ring of integers of \(\mathbb{Q}(i\sqrt{D}) \subseteq \mathbb{C}\) generated by \(a\) and \((b + i\sqrt{D})/2\) is nonzero.

theorem formIdeal_ne_zero (D : ℕ) (q : ℤ × ℤ × ℤ) (ha : q.1 ≠ 0) :
    formIdeal D q ≠ 0

Uses 4 · Used by 1

Statement usesIdeal of a binary quadratic form · The imaginary quadratic field \(\mathbb{Q}(\sqrt{-D})\)

Proof usesThe imaginary square root of \(-D\) · The imaginary root is integral over \(\mathbb{Q}\)

Used byIdeal class of a binary quadratic form

DefinitionIdeal class of a binary quadratic form#✓fully proved

Let \(D\) be a natural number, let \(K = \mathbb{Q}(i\sqrt{D}) \subseteq \mathbb{C}\) and let \(\mathcal{O}_K\) be its ring of integers. For integers \(a, b, c\) with \(a \ne 0\), the ideal class of the triple \((a, b, c)\) is the class, in the class group of \(\mathcal{O}_K\), of the nonzero fractional ideal of \(\mathcal{O}_K\) in \(K\) generated by \(a\) and \((b + i\sqrt{D})/2\).

def classOfForm (D : ℕ) (q : ℤ × ℤ × ℤ) (ha : q.1 ≠ 0) :
    ClassGroup (𝓞 (imaginaryQuadraticField D)) :=
  ClassGroup.mk (imaginaryQuadraticField D) (Units.mk0 (formIdeal D q)
    (formIdeal_ne_zero D q ha))

Uses 5

Statement usesIdeal of a binary quadratic form · The ideal of a form is nonzero · The imaginary quadratic field \(\mathbb{Q}(\sqrt{-D})\) · The imaginary square root of \(-D\) · The imaginary root is integral over \(\mathbb{Q}\)

DefinitionGauss-reduced binary quadratic forms#✓fully proved

The integral binary quadratic form \(a x^2 + b x y + c y^2\) is Gauss reduced when \(a > 0\), its discriminant \(b^2 - 4ac\) is negative, \(|b| \le a \le c\), and \(b \ge 0\) whenever \(|b| = a\) or \(a = c\).

For example, \(x^2 - x y + y^2\) is positive definite and satisfies \(|b| \le a \le c\), but it is not reduced, because \(|b| = a\) and \(b < 0\).

def IsGaussReduced (a b c : ℤ) : Prop :=
  0 < a ∧ discrim a b c < 0 ∧ |b| ≤ a ∧ a ≤ c ∧
    ((|b| = a ∨ a = c) → 0 ≤ b)

Sources

• Mortenson, A Kronecker-type identity, Bull. LMS 49 (2017), arXiv:1702.01627v2, Section 2, line 259.

Used by 1

Used byReduced forms of a given discriminant

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.