Content and primitive forms of fixed discriminant

The content of an integral binary quadratic form is the nonnegative gcd of its three coefficients. Dividing by it gives a primitive form whenever the original form is nonzero. The content is also the gcd of all represented values, which makes it invariant under proper integral changes of variables. Scaling the form multiplies its content by the absolute value of the scalar and its discriminant by the scalar's square. Dividing a nonzero integer vector by its gcd gives coprime coordinates and divides every represented value by the square of that gcd.

The invariance of discriminant and primitivity packages primitive forms of a fixed discriminant in the subaction primitiveForms D, stable under SL(2, ℤ). This gives the carrier for proper-equivalence and orbit constructions among forms of that discriminant. Intersecting with the positive definite forms gives PosDefProperClass n, the proper equivalence classes of primitive positive definite forms of discriminant -n.

Two forms (a, B, a'C) and (a', B, aC) sharing the middle coefficient have Dirichlet composition (aa', B, C), of the same discriminant B² - 4aa'C; if both are primitive so is the composition (isPrimitive_mk_mul_of_isPrimitive). The principal form of discriminant D ≡ 0, 1 mod 4 is x² + δxy + ((δ - D)/4)y² with δ = D mod 2 (principalForm); it is primitive of discriminant D, and positive definite when D < 0.

References

• D. A. Cox, Primes of the Form x² + ny², §2, and §3 for Dirichlet composition.

theorem TauCeti.BinaryQuadraticForm.exists_isCoprime_eval_eq_gcd_sq_mul (f : BinaryQuadraticForm ℤ) (x y : ℤ) (hxy : x ≠ 0 ∨ y ≠ 0) : ∃ (u : ℤ) (v : ℤ), IsCoprime u v ∧ x = u * ↑(x.gcd y) ∧ y = v * ↑(x.gcd y) ∧ f.eval x y = ↑(x.gcd y) ^ 2 * f.eval u v

Dividing a nonzero integer vector by its gcd gives coprime coordinates and scales its represented value by the square of the gcd.

def TauCeti.BinaryQuadraticForm.content (f : BinaryQuadraticForm ℤ) : ℕ

The nonnegative gcd of the three coefficients of an integral binary quadratic form.

theorem TauCeti.BinaryQuadraticForm.content_def (f : BinaryQuadraticForm ℤ) : f.content = f.a.gcd ↑(f.b.gcd f.c)

The content is the gcd of the leading coefficient and the gcd of the other two.

@[simp]

theorem TauCeti.BinaryQuadraticForm.content_zero : content 0 = 0

The zero form has content zero.

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

An integral binary quadratic form is primitive when its coefficients have gcd one.

theorem TauCeti.BinaryQuadraticForm.isPrimitive_iff (f : BinaryQuadraticForm ℤ) : f.IsPrimitive ↔ f.content = 1

Primitivity is equivalent to content one.

@[simp]

theorem TauCeti.BinaryQuadraticForm.not_isPrimitive_zero : ¬IsPrimitive 0

The zero form is not primitive.

theorem TauCeti.BinaryQuadraticForm.IsPrimitive.ne_zero {f : BinaryQuadraticForm ℤ} (hf : f.IsPrimitive) : f ≠ 0

A primitive integral form is nonzero.

theorem TauCeti.BinaryQuadraticForm.exists_linearCombination_eq_content (f : BinaryQuadraticForm ℤ) : ∃ (u : ℤ) (v : ℤ) (w : ℤ), u * f.a + v * f.b + w * f.c = ↑f.content

The coefficients of an integral form have a Bézout relation for its content.

theorem TauCeti.BinaryQuadraticForm.IsPrimitive.exists_linearCombination_eq_one {f : BinaryQuadraticForm ℤ} (hf : f.IsPrimitive) : ∃ (u : ℤ) (v : ℤ) (w : ℤ), u * f.a + v * f.b + w * f.c = 1

The coefficients of a primitive form have an integral Bézout relation.

theorem TauCeti.BinaryQuadraticForm.IsPrimitive.span_intCast_eq_top {R : Type u_1} [CommRing R] {f : BinaryQuadraticForm ℤ} (hf : f.IsPrimitive) : Ideal.span {↑f.a, ↑f.b, ↑f.c} = ⊤

The coefficients of a primitive form generate the unit ideal of every commutative ring R.

theorem TauCeti.BinaryQuadraticForm.dvd_content_iff (f : BinaryQuadraticForm ℤ) (n : ℕ) : n ∣ f.content ↔ ↑n ∣ f.a ∧ ↑n ∣ f.b ∧ ↑n ∣ f.c

A natural number divides the content exactly when it divides all three coefficients.

theorem TauCeti.BinaryQuadraticForm.content_dvd_a (f : BinaryQuadraticForm ℤ) : ↑f.content ∣ f.a

The content divides the leading coefficient.

theorem TauCeti.BinaryQuadraticForm.content_dvd_b (f : BinaryQuadraticForm ℤ) : ↑f.content ∣ f.b

The content divides the middle coefficient.

theorem TauCeti.BinaryQuadraticForm.content_dvd_c (f : BinaryQuadraticForm ℤ) : ↑f.content ∣ f.c

The content divides the last coefficient.

theorem TauCeti.BinaryQuadraticForm.isPrimitive_of_linearCombination_eq_one (f : BinaryQuadraticForm ℤ) (u v w : ℤ) (h : u * f.a + v * f.b + w * f.c = 1) : f.IsPrimitive

An integral Bézout relation among the coefficients makes the form primitive.

@[simp]

theorem TauCeti.BinaryQuadraticForm.content_eq_zero_iff (f : BinaryQuadraticForm ℤ) : f.content = 0 ↔ f = 0

Content zero occurs exactly for the form with all coefficients zero.

theorem TauCeti.BinaryQuadraticForm.content_pos_iff (f : BinaryQuadraticForm ℤ) : 0 < f.content ↔ f ≠ 0

Every nonzero binary quadratic form has positive content.

@[simp]

theorem TauCeti.BinaryQuadraticForm.content_smul' (f : BinaryQuadraticForm ℤ) (r : ℤ) : (r • f).content = r.natAbs * f.content

The content of a scalar multiple is the absolute scalar times the original content.

@[simp]

theorem TauCeti.BinaryQuadraticForm.content_nsmul (f : BinaryQuadraticForm ℤ) (n : ℕ) : (n • f).content = n * f.content

Natural scalar multiplication multiplies the content by that scalar.

@[simp]

theorem TauCeti.BinaryQuadraticForm.content_neg (f : BinaryQuadraticForm ℤ) : (-f).content = f.content

Negation preserves the content.

def TauCeti.BinaryQuadraticForm.primPart (f : BinaryQuadraticForm ℤ) : BinaryQuadraticForm ℤ

Divide all three coefficients by the content. The zero form has zero primitive part.

@[simp]

theorem TauCeti.BinaryQuadraticForm.primPart_a (f : BinaryQuadraticForm ℤ) : f.primPart.a = f.a / ↑f.content

The leading coefficient of the primitive part.

@[simp]

theorem TauCeti.BinaryQuadraticForm.primPart_b (f : BinaryQuadraticForm ℤ) : f.primPart.b = f.b / ↑f.content

The middle coefficient of the primitive part.

@[simp]

theorem TauCeti.BinaryQuadraticForm.primPart_c (f : BinaryQuadraticForm ℤ) : f.primPart.c = f.c / ↑f.content

The last coefficient of the primitive part.

@[simp]

theorem TauCeti.BinaryQuadraticForm.primPart_zero : primPart 0 = 0

The primitive part of the zero form is zero.

@[simp]

theorem TauCeti.BinaryQuadraticForm.content_smul_primPart (f : BinaryQuadraticForm ℤ) : f.content • f.primPart = f

The original form is its content times its primitive part, including for the zero form.

@[simp]

theorem TauCeti.BinaryQuadraticForm.primPart_eq_zero_iff (f : BinaryQuadraticForm ℤ) : f.primPart = 0 ↔ f = 0

A form has zero primitive part exactly when the form itself is zero.

theorem TauCeti.BinaryQuadraticForm.isPrimitive_primPart (f : BinaryQuadraticForm ℤ) (hf : f ≠ 0) : f.primPart.IsPrimitive

The primitive part of a nonzero form has content one.

@[simp]

theorem TauCeti.BinaryQuadraticForm.IsPrimitive.primPart_eq {f : BinaryQuadraticForm ℤ} (hf : f.IsPrimitive) : f.primPart = f

A primitive form is its own primitive part.

theorem TauCeti.BinaryQuadraticForm.content_smul_of_isPrimitive (f : BinaryQuadraticForm ℤ) (r : ℤ) (hf : f.IsPrimitive) : (r • f).content = r.natAbs

A scalar multiple of a primitive form has content the absolute scalar.

theorem TauCeti.BinaryQuadraticForm.primPart_smul' (f : BinaryQuadraticForm ℤ) (r : ℤ) : (r • f).primPart = r.sign • f.primPart

Primitive normalization of a scalar multiple retains only the sign of the scalar. The formula also holds when either the scalar or the form is zero.

theorem TauCeti.BinaryQuadraticForm.primPart_smul_of_isPrimitive (f : BinaryQuadraticForm ℤ) (r : ℤ) (hf : f.IsPrimitive) : (r • f).primPart = r.sign • f

For a primitive form, scalar normalization retains the sign times the form itself.

@[simp]

theorem TauCeti.BinaryQuadraticForm.primPart_neg (f : BinaryQuadraticForm ℤ) : (-f).primPart = -f.primPart

Primitive normalization commutes with negation.

theorem TauCeti.BinaryQuadraticForm.eq_smul_iff_of_isPrimitive (f g : BinaryQuadraticForm ℤ) {c : ℕ} (hc : 0 < c) (hg : g.IsPrimitive) : f = ↑c • g ↔ f.content = c ∧ f.primPart = g

The decomposition into positive content and a primitive form is unique.

theorem TauCeti.BinaryQuadraticForm.discrim_eq_content_sq_mul (f : BinaryQuadraticForm ℤ) : f.discrim = ↑f.content ^ 2 * f.primPart.discrim

A form's discriminant is the square of its content times its primitive discriminant.

theorem TauCeti.BinaryQuadraticForm.dvd_content_iff_forall_eval (f : BinaryQuadraticForm ℤ) (n : ℕ) : n ∣ f.content ↔ ∀ (x y : ℤ), ↑n ∣ f.eval x y

Divisibility of every represented value is equivalent to divisibility of the content.

@[simp]

theorem TauCeti.BinaryQuadraticForm.content_smul (f : BinaryQuadraticForm ℤ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (γ • f).content = f.content

Proper integral changes of variables preserve the content.

@[simp]

theorem TauCeti.BinaryQuadraticForm.isPrimitive_smul_iff (f : BinaryQuadraticForm ℤ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (γ • f).IsPrimitive ↔ f.IsPrimitive

Primitivity is preserved by proper integral changes of variables.

def TauCeti.BinaryQuadraticForm.primitiveForms (D : ℤ) : SubMulAction (Matrix.SpecialLinearGroup (Fin 2) ℤ) (BinaryQuadraticForm ℤ)

Primitive forms of fixed discriminant, with the proper special-linear action.

@[simp]

theorem TauCeti.BinaryQuadraticForm.mem_primitiveForms (D : ℤ) (f : BinaryQuadraticForm ℤ) : f ∈ primitiveForms D ↔ f.discrim = D ∧ f.IsPrimitive

Membership in the primitive fixed-discriminant forms.

@[simp]

theorem TauCeti.BinaryQuadraticForm.mem_posDef_inf_primitiveForms (n : ℕ) [NeZero n] {f : BinaryQuadraticForm ℤ} : f ∈ posDef n ⊓ primitiveForms (-↑n) ↔ f.discrim = -↑n ∧ 0 < f.a ∧ f.IsPrimitive

A form is primitive positive definite of discriminant -n exactly when it has discriminant -n, positive leading coefficient and coprime coefficients.

@[reducible, inline]

abbrev TauCeti.BinaryQuadraticForm.PosDefProperClass (n : ℕ) [NeZero n] : Type

The proper equivalence classes of primitive positive definite forms of discriminant -n.

theorem TauCeti.BinaryQuadraticForm.primPart_smul (f : BinaryQuadraticForm ℤ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (γ • f).primPart = γ • f.primPart

Taking primitive parts commutes with proper integral changes of variables.

@[simp]

theorem TauCeti.BinaryQuadraticForm.stabilizer_primPart (f : BinaryQuadraticForm ℤ) : MulAction.stabilizer (Matrix.SpecialLinearGroup (Fin 2) ℤ) f.primPart = MulAction.stabilizer (Matrix.SpecialLinearGroup (Fin 2) ℤ) f

A form and its primitive part have the same proper automorphs.

@[simp]

theorem TauCeti.BinaryQuadraticForm.discrim_primPart_smul (f : BinaryQuadraticForm ℤ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (γ • f).primPart.discrim = f.primPart.discrim

The discriminant of a primitive part is invariant under proper changes of variables.

Dirichlet composition of united forms

theorem TauCeti.BinaryQuadraticForm.discrim_mk_mul_left (a a' B C : ℤ) : { a := a, b := B, c := a' * C }.discrim = { a := a * a', b := B, c := C }.discrim

The forms (a, B, a'C) and (aa', B, C) have the same discriminant B² - 4aa'C.

theorem TauCeti.BinaryQuadraticForm.discrim_mk_mul_right (a a' B C : ℤ) : { a := a', b := B, c := a * C }.discrim = { a := a * a', b := B, c := C }.discrim

The forms (a', B, aC) and (aa', B, C) have the same discriminant B² - 4aa'C.

theorem TauCeti.BinaryQuadraticForm.isPrimitive_mk_mul_of_isPrimitive {a a' B C : ℤ} (hf : { a := a, b := B, c := a' * C }.IsPrimitive) (hg : { a := a', b := B, c := a * C }.IsPrimitive) : { a := a * a', b := B, c := C }.IsPrimitive

The Dirichlet composition of primitive united forms is primitive. If (a, B, a'C) and (a', B, aC) are primitive, then so is (aa', B, C).

The principal form

def TauCeti.BinaryQuadraticForm.principalForm (D : ℤ) : BinaryQuadraticForm ℤ

The principal form of discriminant D, x² + δxy + ((δ - D)/4)y² with δ = D mod 2. For D ≡ 0, 1 mod 4 it has discriminant D (discrim_principalForm).

@[simp]

theorem TauCeti.BinaryQuadraticForm.principalForm_a (D : ℤ) : (principalForm D).a = 1

The leading coefficient of the principal form is 1.

@[simp]

theorem TauCeti.BinaryQuadraticForm.principalForm_b (D : ℤ) : (principalForm D).b = D % 2

The middle coefficient of the principal form is D mod 2.

@[simp]

theorem TauCeti.BinaryQuadraticForm.principalForm_c (D : ℤ) : (principalForm D).c = (D % 2 - D) / 4

The last coefficient of the principal form is (D mod 2 - D) / 4.

theorem TauCeti.BinaryQuadraticForm.discrim_principalForm {D : ℤ} (hD : D % 4 = 0 ∨ D % 4 = 1) : (principalForm D).discrim = D

The principal form of discriminant D ≡ 0, 1 mod 4 has discriminant D.

theorem TauCeti.BinaryQuadraticForm.isPrimitive_principalForm (D : ℤ) : (principalForm D).IsPrimitive

The principal form is primitive.

theorem TauCeti.BinaryQuadraticForm.principalForm_mem_primitiveForms {D : ℤ} (hD : D % 4 = 0 ∨ D % 4 = 1) : principalForm D ∈ primitiveForms D

The principal form is a primitive form of discriminant D ≡ 0, 1 mod 4.

theorem TauCeti.BinaryQuadraticForm.principalForm_mem_posDef_inf_primitiveForms (n : ℕ) [NeZero n] (hn : -↑n % 4 = 0 ∨ -↑n % 4 = 1) : principalForm (-↑n) ∈ posDef n ⊓ primitiveForms (-↑n)

The principal form of discriminant -n is primitive positive definite.