Binary quadratic forms and the action of SL(2, R)

A binary quadratic form over a commutative ring R is a polynomial a x² + b x y + c y²; here it is recorded by its three coefficients, as TauCeti.BinaryQuadraticForm R. The group SL(2, R) acts on such forms by linear change of variables, and over ℤ the forms that are positive definite of a fixed discriminant -D < 0 form a sub-action. Its orbits are the classes counted, with weights, by the Hurwitz class number H(D) (TauCeti.hurwitzClassNumber). Through the form v ↦ det(v, M v) attached to an integer matrix M, they also describe the SL(2, ℤ)-conjugacy classes of integer matrices of fixed trace and determinant, which is how they enter the Eichler–Selberg trace formula. This file supplies the action on which both descriptions are built.

The action is on the left, by γ • f = f ∘ γ⁻¹. For γ = !![p, q; r, s] the inverse is the adjugate !![s, -q; -r, p] (Mathlib's Matrix.SpecialLinearGroup.SL2_inv_expl), so (γ • f)(x, y) = f(s x - q y, -r x + p y) and the new coefficients are

a' = a s² - b r s + c r²
b' = b (p s + q r) - 2 a q s - 2 c p r
c' = a q² - b p q + c p².

Only the entries of the adjugate occur, so the action laws are polynomial identities and need no determinant hypothesis. The substitution f ↦ f ∘ γ found in much of the classical literature is a right action; composing with γ⁻¹ instead gives the left action that MulAction expects, with the same orbits. With this convention T • ⟨a, b, c⟩ = ⟨a, b - 2 a, a - b + c⟩ and S • ⟨a, b, c⟩ = ⟨c, -b, a⟩, where S and T are Mathlib's ModularGroup.S = !![0, -1; 1, 0] and ModularGroup.T = !![1, 1; 0, 1] (T_smul, S_smul). It is also the convention for which the root (-b + √(-D)) / (2 a) of a positive definite form moves by the Möbius action of γ on the upper half-plane.

The discriminant discrim a b c = b² - 4 a c changes by the factor (det γ)² = 1. Positivity of the leading coefficient is then preserved: (γ • f).a = f(s, -r) is a value of the non-negative form f, and a form of negative discriminant with non-negative leading coefficient has positive leading coefficient. This needs D ≠ 0: the form ⟨1, 2, 1⟩ of discriminant 0 is sent by !![1, 0; 1, 1] to a form with leading coefficient 0.

Mathlib's QuadraticForm R (Fin 2 → R) is not used, because its discriminant is built from the associated bilinear form and so requires 2 to be invertible in R, which fails over ℤ.

Main definitions

• TauCeti.BinaryQuadraticForm R: the binary quadratic form a x² + b x y + c y² over R.
• TauCeti.BinaryQuadraticForm.equivProd: a form is its triple of coefficients (a, b, c).
• Binary quadratic forms inherit coefficientwise addition and scalar multiplication, including Module S (TauCeti.BinaryQuadraticForm R) whenever R is an S-module.
• TauCeti.BinaryQuadraticForm.discrim: its discriminant b² - 4 a c.
• TauCeti.BinaryQuadraticForm.eval: its value a x² + b x y + c y² at (x, y).
• TauCeti.BinaryQuadraticForm.map: the form with coefficients mapped along a ring homomorphism, for instance an integral form read over ℤ_p or ℚ.
• The instance MulAction SL(2, R) (TauCeti.BinaryQuadraticForm R): the action γ • f = f ∘ γ⁻¹, for a commutative ring R.
• TauCeti.BinaryQuadraticForm.posDef D: for D ≠ 0, the positive definite integral forms of discriminant -D, as a sub-action of SL(2, ℤ).

Main results

• TauCeti.BinaryQuadraticForm.smul_a, TauCeti.BinaryQuadraticForm.smul_b and TauCeti.BinaryQuadraticForm.smul_c: the coefficients of γ • f.
• TauCeti.BinaryQuadraticForm.eval_smul: γ • f is f ∘ γ⁻¹.
• TauCeti.BinaryQuadraticForm.discrim_smul: the discriminant is invariant under SL(2, R).
• TauCeti.BinaryQuadraticForm.smul_map: mapping coefficients is equivariant for the entrywise map SL(2, R) →* SL(2, S), so automorphs map to automorphs (TauCeti.BinaryQuadraticForm.map_mem_stabilizer_map).
• TauCeti.BinaryQuadraticForm.T_zpow_smul, TauCeti.BinaryQuadraticForm.T_smul and TauCeti.BinaryQuadraticForm.S_smul: the action of T ^ k, T and S on coefficients.
• TauCeti.BinaryQuadraticForm.isUnit_det_of_quadratic_identity: a coordinate change producing a unit discriminant has unit determinant over any commutative ring.
• TauCeti.BinaryQuadraticForm.mem_posDef: membership in posDef D.

Implementation notes

discrim and equivProd are exposed, so that the kernel can evaluate them, as decide does for the values of TauCeti.hurwitzClassNumber. The additive coefficient equivalence addEquivProd is also exposed to transport the module structure.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, Graduate Texts in Mathematics 138, Springer, 1993, §5.2–5.3.
• D. A. Buell, Binary Quadratic Forms: Classical Theory and Modern Computations, Springer, 1989.
• 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.

structure TauCeti.BinaryQuadraticForm (R : Type u_1) : Type u_1

A binary quadratic form a x² + b x y + c y² over R, recorded by its three coefficients.

• a : R

  The coefficient of x².

• b : R

  The coefficient of x y.

• c : R

  The coefficient of y².

theorem TauCeti.BinaryQuadraticForm.ext {R : Type u_1} {x y : BinaryQuadraticForm R} (a : x.a = y.a) (b : x.b = y.b) (c : x.c = y.c) : x = y

theorem TauCeti.BinaryQuadraticForm.ext_iff {R : Type u_1} {x y : BinaryQuadraticForm R} : x = y ↔ x.a = y.a ∧ x.b = y.b ∧ x.c = y.c

def TauCeti.instDecidableEqBinaryQuadraticForm.decEq {R✝ : Type u_1} [DecidableEq R✝] (x✝ x✝¹ : BinaryQuadraticForm R✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TauCeti.instDecidableEqBinaryQuadraticForm {R✝ : Type u_1} [DecidableEq R✝] : DecidableEq (BinaryQuadraticForm R✝)

def TauCeti.BinaryQuadraticForm.equivProd {R : Type u_1} : BinaryQuadraticForm R ≃ R × R × R

A binary quadratic form is its triple of coefficients (a, b, c).

@[simp]

theorem TauCeti.BinaryQuadraticForm.equivProd_symm_apply_b {R : Type u_1} (t : R × R × R) : (equivProd.symm t).b = t.2.1

@[simp]

theorem TauCeti.BinaryQuadraticForm.equivProd_symm_apply_a {R : Type u_1} (t : R × R × R) : (equivProd.symm t).a = t.1

@[simp]

theorem TauCeti.BinaryQuadraticForm.equivProd_symm_apply_c {R : Type u_1} (t : R × R × R) : (equivProd.symm t).c = t.2.2

@[simp]

theorem TauCeti.BinaryQuadraticForm.equivProd_apply {R : Type u_1} (f : BinaryQuadraticForm R) : equivProd f = (f.a, f.b, f.c)

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instZero {R : Type u_1} [Zero R] : Zero (BinaryQuadraticForm R)

The zero binary quadratic form has zero coefficients.

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instAdd {R : Type u_1} [Add R] : Add (BinaryQuadraticForm R)

Addition of binary quadratic forms is coefficientwise.

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instNeg {R : Type u_1} [Neg R] : Neg (BinaryQuadraticForm R)

Negation of binary quadratic forms is coefficientwise.

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instSub {R : Type u_1} [Sub R] : Sub (BinaryQuadraticForm R)

Subtraction of binary quadratic forms is coefficientwise.

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instSMul {S : Type u_1} {R : Type u_2} [SMul S R] : SMul S (BinaryQuadraticForm R)

Scalar multiplication acts coefficientwise on binary quadratic forms.

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instAddCommMonoid {R : Type u_1} [AddCommMonoid R] : AddCommMonoid (BinaryQuadraticForm R)

Addition of binary quadratic forms is coefficientwise.

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instAddCommGroup {R : Type u_1} [AddCommGroup R] : AddCommGroup (BinaryQuadraticForm R)

Binary quadratic forms over an additive group form an additive group.

def TauCeti.BinaryQuadraticForm.addEquivProd {R : Type u_1} [AddCommMonoid R] : BinaryQuadraticForm R ≃+ R × R × R

The additive coefficient equivalence used to transport the module structure.

@[simp]

theorem TauCeti.BinaryQuadraticForm.addEquivProd_symm_apply_b {R : Type u_1} [AddCommMonoid R] (t : R × R × R) : (addEquivProd.symm t).b = t.2.1

@[simp]

theorem TauCeti.BinaryQuadraticForm.addEquivProd_apply {R : Type u_1} [AddCommMonoid R] (f : BinaryQuadraticForm R) : addEquivProd f = (f.a, f.b, f.c)

@[simp]

theorem TauCeti.BinaryQuadraticForm.addEquivProd_symm_apply_a {R : Type u_1} [AddCommMonoid R] (t : R × R × R) : (addEquivProd.symm t).a = t.1

@[simp]

theorem TauCeti.BinaryQuadraticForm.addEquivProd_symm_apply_c {R : Type u_1} [AddCommMonoid R] (t : R × R × R) : (addEquivProd.symm t).c = t.2.2

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instModule {S : Type u_1} {R : Type u_2} [Semiring S] [AddCommMonoid R] [Module S R] : Module S (BinaryQuadraticForm R)

A module structure on the coefficients induces one on binary quadratic forms.

instance TauCeti.BinaryQuadraticForm.instModuleIsTorsionFree {S : Type u_1} {R : Type u_2} [Semiring S] [AddCommMonoid R] [Module S R] [Module.IsTorsionFree S R] : Module.IsTorsionFree S (BinaryQuadraticForm R)

Regular scalars act injectively on binary quadratic forms.

@[simp]

theorem TauCeti.BinaryQuadraticForm.zero_a {R : Type u_1} [Zero R] : a 0 = 0

The leading coefficient of the zero form is zero.

@[simp]

theorem TauCeti.BinaryQuadraticForm.zero_b {R : Type u_1} [Zero R] : b 0 = 0

The middle coefficient of the zero form is zero.

@[simp]

theorem TauCeti.BinaryQuadraticForm.zero_c {R : Type u_1} [Zero R] : c 0 = 0

The last coefficient of the zero form is zero.

@[simp]

theorem TauCeti.BinaryQuadraticForm.add_a {R : Type u_1} [Add R] (f g : BinaryQuadraticForm R) : (f + g).a = f.a + g.a

Addition adds the leading coefficients.

@[simp]

theorem TauCeti.BinaryQuadraticForm.add_b {R : Type u_1} [Add R] (f g : BinaryQuadraticForm R) : (f + g).b = f.b + g.b

Addition adds the middle coefficients.

@[simp]

theorem TauCeti.BinaryQuadraticForm.add_c {R : Type u_1} [Add R] (f g : BinaryQuadraticForm R) : (f + g).c = f.c + g.c

Addition adds the last coefficients.

@[simp]

theorem TauCeti.BinaryQuadraticForm.neg_a {R : Type u_1} [Neg R] (f : BinaryQuadraticForm R) : (-f).a = -f.a

Negation negates the leading coefficient.

@[simp]

theorem TauCeti.BinaryQuadraticForm.neg_b {R : Type u_1} [Neg R] (f : BinaryQuadraticForm R) : (-f).b = -f.b

Negation negates the middle coefficient.

@[simp]

theorem TauCeti.BinaryQuadraticForm.neg_c {R : Type u_1} [Neg R] (f : BinaryQuadraticForm R) : (-f).c = -f.c

Negation negates the last coefficient.

@[simp]

theorem TauCeti.BinaryQuadraticForm.sub_a {R : Type u_1} [Sub R] (f g : BinaryQuadraticForm R) : (f - g).a = f.a - g.a

Subtraction subtracts the leading coefficients.

@[simp]

theorem TauCeti.BinaryQuadraticForm.sub_b {R : Type u_1} [Sub R] (f g : BinaryQuadraticForm R) : (f - g).b = f.b - g.b

Subtraction subtracts the middle coefficients.

@[simp]

theorem TauCeti.BinaryQuadraticForm.sub_c {R : Type u_1} [Sub R] (f g : BinaryQuadraticForm R) : (f - g).c = f.c - g.c

Subtraction subtracts the last coefficients.

@[simp]

theorem TauCeti.BinaryQuadraticForm.smul_a' {R : Type u_1} {S : Type u_2} [SMul S R] (r : S) (f : BinaryQuadraticForm R) : (r • f).a = r • f.a

Scalar multiplication multiplies the leading coefficient.

@[simp]

theorem TauCeti.BinaryQuadraticForm.smul_b' {R : Type u_1} {S : Type u_2} [SMul S R] (r : S) (f : BinaryQuadraticForm R) : (r • f).b = r • f.b

Scalar multiplication multiplies the middle coefficient.

@[simp]

theorem TauCeti.BinaryQuadraticForm.smul_c' {R : Type u_1} {S : Type u_2} [SMul S R] (r : S) (f : BinaryQuadraticForm R) : (r • f).c = r • f.c

Scalar multiplication multiplies the last coefficient.

def TauCeti.BinaryQuadraticForm.eval {R : Type u_1} [Semiring R] (f : BinaryQuadraticForm R) (x y : R) : R

The value a x² + b x y + c y² of the form f at (x, y).

theorem TauCeti.BinaryQuadraticForm.eval_def {R : Type u_1} [Semiring R] (f : BinaryQuadraticForm R) (x y : R) : f.eval x y = f.a * x ^ 2 + f.b * x * y + f.c * y ^ 2

The value of f at (x, y) is a x² + b x y + c y².

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_mk {R : Type u_1} [Semiring R] (a b c x y : R) : { a := a, b := b, c := c }.eval x y = a * x ^ 2 + b * x * y + c * y ^ 2

The value of the form ⟨a, b, c⟩ at (x, y) is a x² + b x y + c y².

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_one_zero {R : Type u_1} [Semiring R] (f : BinaryQuadraticForm R) : f.eval 1 0 = f.a

The value of f at (1, 0) is its first coefficient a.

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_zero_one {R : Type u_1} [Semiring R] (f : BinaryQuadraticForm R) : f.eval 0 1 = f.c

The value of f at (0, 1) is its last coefficient c.

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_zero {R : Type u_1} [Semiring R] (x y : R) : eval 0 x y = 0

The zero form represents only zero.

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_add {R : Type u_1} [Semiring R] (f g : BinaryQuadraticForm R) (x y : R) : (f + g).eval x y = f.eval x y + g.eval x y

Evaluation respects addition of forms.

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_smul' {R : Type u_1} [Semiring R] (r : R) (f : BinaryQuadraticForm R) (x y : R) : (r • f).eval x y = r * f.eval x y

Scaling a form multiplies every represented value by the scalar.

def TauCeti.BinaryQuadraticForm.evalLinearMap {R : Type u_1} [Semiring R] (x y : R) : BinaryQuadraticForm R →ₗ[R] R

Evaluation at fixed coordinates is linear in the coefficients of the form.

@[simp]

theorem TauCeti.BinaryQuadraticForm.evalLinearMap_apply {R : Type u_1} [Semiring R] (x y : R) (f : BinaryQuadraticForm R) : (evalLinearMap x y) f = f.eval x y

The evaluation linear map evaluates the form at its fixed coordinates.

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_nsmul {R : Type u_1} [Semiring R] (n : ℕ) (f : BinaryQuadraticForm R) (x y : R) : (n • f).eval x y = n • f.eval x y

Evaluation respects natural scalar multiplication.

def TauCeti.BinaryQuadraticForm.map {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (φ : R →+* S) (f : BinaryQuadraticForm R) : BinaryQuadraticForm S

The form φ(a) x² + φ(b) x y + φ(c) y² obtained by applying φ : R →+* S to the coefficients of f = a x² + b x y + c y².

@[simp]

theorem TauCeti.BinaryQuadraticForm.map_a {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (φ : R →+* S) (f : BinaryQuadraticForm R) : (map φ f).a = φ f.a

@[simp]

theorem TauCeti.BinaryQuadraticForm.map_b {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (φ : R →+* S) (f : BinaryQuadraticForm R) : (map φ f).b = φ f.b

@[simp]

theorem TauCeti.BinaryQuadraticForm.map_c {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (φ : R →+* S) (f : BinaryQuadraticForm R) : (map φ f).c = φ f.c

@[simp]

theorem TauCeti.BinaryQuadraticForm.map_id {R : Type u_1} [Semiring R] (f : BinaryQuadraticForm R) : map (RingHom.id R) f = f

@[simp]

theorem TauCeti.BinaryQuadraticForm.map_map {R : Type u_1} [Semiring R] {S : Type u_2} {T : Type u_3} [Semiring S] [Semiring T] (φ : R →+* S) (ψ : S →+* T) (f : BinaryQuadraticForm R) : map ψ (map φ f) = map (ψ.comp φ) f

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_map {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (φ : R →+* S) (f : BinaryQuadraticForm R) (x y : R) : (map φ f).eval (φ x) (φ y) = φ (f.eval x y)

Mapping the coefficients maps the values: (f.map φ)(φ x, φ y) = φ (f(x, y)).

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_neg {R : Type u_1} [Ring R] (f : BinaryQuadraticForm R) (x y : R) : (-f).eval x y = -f.eval x y

Evaluation respects negation of forms.

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_sub {R : Type u_1} [Ring R] (f g : BinaryQuadraticForm R) (x y : R) : (f - g).eval x y = f.eval x y - g.eval x y

Evaluation respects subtraction of forms.

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_zsmul {R : Type u_1} [Ring R] (n : ℤ) (f : BinaryQuadraticForm R) (x y : R) : (n • f).eval x y = n • f.eval x y

Evaluation respects integer scalar multiplication.

theorem TauCeti.BinaryQuadraticForm.isUnit_det_of_quadratic_identity {R : Type u_1} [CommRing R] {a b u e₁ e₂ f₁ f₂ A B C : R} (hdisc : IsUnit (4 * A * B - C ^ 2)) (h : ∀ (m n : R), a * (m * e₁ + n * f₁) ^ 2 + u * (m * e₁ + n * f₁) * (m * e₂ + n * f₂) + b * (m * e₂ + n * f₂) ^ 2 = A * m ^ 2 + C * m * n + B * n ^ 2) : IsUnit (e₁ * f₂ - f₁ * e₂)

If the binary form am² + umn + bn² becomes Am² + Cmn + Bn² under the coordinate change with matrix !![e₁, f₁; e₂, f₂], and 4AB - C² is a unit, then that matrix has unit determinant: the discriminants satisfy 4AB - C² = (e₁f₂ - f₁e₂)² (4ab - u²).

def TauCeti.BinaryQuadraticForm.discrim {R : Type u_1} [CommRing R] (f : BinaryQuadraticForm R) : R

The discriminant b² - 4 a c of the form a x² + b x y + c y².

theorem TauCeti.BinaryQuadraticForm.discrim_def {R : Type u_1} [CommRing R] (f : BinaryQuadraticForm R) : f.discrim = discrim f.a f.b f.c

The discriminant of a form is Mathlib's discrim of its coefficients.

theorem TauCeti.BinaryQuadraticForm.discrim_emod_four_eq_zero_or_one (f : BinaryQuadraticForm ℤ) : f.discrim % 4 = 0 ∨ f.discrim % 4 = 1

The discriminant of an integral binary form is zero or one modulo four.

theorem TauCeti.BinaryQuadraticForm.a_ne_zero_of_not_isSquare_discrim {f : BinaryQuadraticForm ℤ} (hf : ¬IsSquare f.discrim) : f.a ≠ 0

A form of nonsquare discriminant has nonzero leading coefficient.

theorem TauCeti.BinaryQuadraticForm.c_ne_zero_of_not_isSquare_discrim {f : BinaryQuadraticForm ℤ} (hf : ¬IsSquare f.discrim) : f.c ≠ 0

A form of nonsquare discriminant has nonzero last coefficient.

instance TauCeti.BinaryQuadraticForm.neZero_of_fact_not_isSquare {D : ℤ} [Fact ¬IsSquare D] : NeZero D

A nonsquare discriminant is nonzero, since 0 = 0 * 0 is a square. This lets results stated under [NeZero D] apply under the standing assumption [Fact (¬ IsSquare D)].

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instSMulSpecialLinearGroupFinOfNatNat {R : Type u_1} [CommRing R] : SMul (Matrix.SpecialLinearGroup (Fin 2) R) (BinaryQuadraticForm R)

γ • f is the form f ∘ γ⁻¹ (eval_smul). The coefficients are written through the entries of the adjugate γ⁻¹ = !![s, -q; -r, p] of γ = !![p, q; r, s], so each is a polynomial in the entries of γ.

@[simp]

theorem TauCeti.BinaryQuadraticForm.smul_a {R : Type u_1} [CommRing R] (γ : Matrix.SpecialLinearGroup (Fin 2) R) (f : BinaryQuadraticForm R) : (γ • f).a = f.a * ↑γ 1 1 ^ 2 - f.b * ↑γ 1 0 * ↑γ 1 1 + f.c * ↑γ 1 0 ^ 2

The x²-coefficient of γ • f is f(s, -r) = a s² - b r s + c r², for γ = !![p, q; r, s].

@[simp]

theorem TauCeti.BinaryQuadraticForm.smul_b {R : Type u_1} [CommRing R] (γ : Matrix.SpecialLinearGroup (Fin 2) R) (f : BinaryQuadraticForm R) : (γ • f).b = f.b * (↑γ 0 0 * ↑γ 1 1 + ↑γ 0 1 * ↑γ 1 0) - 2 * f.a * ↑γ 0 1 * ↑γ 1 1 - 2 * f.c * ↑γ 0 0 * ↑γ 1 0

The x y-coefficient of γ • f is b (p s + q r) - 2 a q s - 2 c p r, for γ = !![p, q; r, s].

@[simp]

theorem TauCeti.BinaryQuadraticForm.smul_c {R : Type u_1} [CommRing R] (γ : Matrix.SpecialLinearGroup (Fin 2) R) (f : BinaryQuadraticForm R) : (γ • f).c = f.a * ↑γ 0 1 ^ 2 - f.b * ↑γ 0 0 * ↑γ 0 1 + f.c * ↑γ 0 0 ^ 2

The y²-coefficient of γ • f is f(-q, p) = a q² - b p q + c p², for γ = !![p, q; r, s].

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_smul {R : Type u_1} [CommRing R] (γ : Matrix.SpecialLinearGroup (Fin 2) R) (f : BinaryQuadraticForm R) (x y : R) : (γ • f).eval x y = f.eval (↑γ 1 1 * x - ↑γ 0 1 * y) (-↑γ 1 0 * x + ↑γ 0 0 * y)

γ • f is f ∘ γ⁻¹: its value at (x, y) is f(s x - q y, -r x + p y), for γ = !![p, q; r, s].

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instMulActionSpecialLinearGroupFinOfNatNat {R : Type u_1} [CommRing R] : MulAction (Matrix.SpecialLinearGroup (Fin 2) R) (BinaryQuadraticForm R)

f ↦ f ∘ γ⁻¹ is a left action of SL(2, R) on binary quadratic forms.

@[instance_reducible]

instance TauCeti.BinaryQuadraticForm.instDistribMulAction {R : Type u_1} [CommRing R] : DistribMulAction (Matrix.SpecialLinearGroup (Fin 2) R) (BinaryQuadraticForm R)

Proper changes of variables act additively on forms.

instance TauCeti.BinaryQuadraticForm.instSMulCommClass {R : Type u_1} [CommRing R] : SMulCommClass R (Matrix.SpecialLinearGroup (Fin 2) R) (BinaryQuadraticForm R)

Scaling the coefficients commutes with a proper change of variables.

theorem TauCeti.BinaryQuadraticForm.exists_smul_a_eq_eval {R : Type u_1} [CommRing R] (f : BinaryQuadraticForm R) {x y : R} (hxy : IsCoprime x y) : ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) R), (γ • f).a = f.eval x y

A primitively represented value can be moved to the leading coefficient by a proper change.

@[simp]

theorem TauCeti.BinaryQuadraticForm.discrim_smul {R : Type u_1} [CommRing R] (γ : Matrix.SpecialLinearGroup (Fin 2) R) (f : BinaryQuadraticForm R) : (γ • f).discrim = f.discrim

The discriminant b² - 4 a c of a binary quadratic form is invariant under SL(2, R).

@[simp]

theorem TauCeti.BinaryQuadraticForm.discrim_smul' {R : Type u_1} [CommRing R] (r : R) (f : BinaryQuadraticForm R) : (r • f).discrim = r ^ 2 * f.discrim

Scaling a form multiplies its discriminant by the squared scalar.

theorem TauCeti.BinaryQuadraticForm.discrim_natCast_smul_eq_neg_iff {D g : ℕ} (hg : g ^ 2 ∣ D) (hg0 : g ≠ 0) (f : BinaryQuadraticForm ℤ) : (↑g • f).discrim = -↑D ↔ f.discrim = -↑(D / g ^ 2)

A form g • f has discriminant -D exactly when f has discriminant -D / g².

@[simp]

theorem TauCeti.BinaryQuadraticForm.discrim_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) (f : BinaryQuadraticForm R) : (map φ f).discrim = φ f.discrim

Mapping the coefficients maps the discriminant.

@[simp]

theorem TauCeti.BinaryQuadraticForm.smul_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) (γ : Matrix.SpecialLinearGroup (Fin 2) R) (f : BinaryQuadraticForm R) : (Matrix.SpecialLinearGroup.map φ) γ • map φ f = map φ (γ • f)

Mapping the coefficients is equivariant for the action of SL(2, R) on forms, through the entrywise map SL(2, R) →* SL(2, S).

theorem TauCeti.BinaryQuadraticForm.map_mem_stabilizer_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) {f : BinaryQuadraticForm R} {γ : Matrix.SpecialLinearGroup (Fin 2) R} (hγ : γ ∈ MulAction.stabilizer (Matrix.SpecialLinearGroup (Fin 2) R) f) : (Matrix.SpecialLinearGroup.map φ) γ ∈ MulAction.stabilizer (Matrix.SpecialLinearGroup (Fin 2) S) (map φ f)

An automorph of f over R maps to an automorph of f.map φ over S.

def TauCeti.BinaryQuadraticForm.posDef (D : ℕ) [NeZero D] : SubMulAction (Matrix.SpecialLinearGroup (Fin 2) ℤ) (BinaryQuadraticForm ℤ)

The positive definite integral binary quadratic forms of discriminant -D, for D ≠ 0, as a sub-action of SL(2, ℤ): the forms of discriminant -D whose leading coefficient is positive.

@[simp]

theorem TauCeti.BinaryQuadraticForm.mem_posDef {D : ℕ} [NeZero D] {f : BinaryQuadraticForm ℤ} : f ∈ posDef D ↔ f.discrim = -↑D ∧ 0 < f.a

A form lies in posDef D exactly when its discriminant is -D and its leading coefficient is positive.

@[simp]

theorem TauCeti.BinaryQuadraticForm.T_zpow_smul (k : ℤ) (f : BinaryQuadraticForm ℤ) : ModularGroup.T ^ k • f = { a := f.a, b := f.b - 2 * f.a * k, c := f.a * k ^ 2 - f.b * k + f.c }

The translation T ^ k sends a x² + b x y + c y² to a x² + (b - 2 a k) x y + (a k² - b k + c) y², the form f(x - k y, y).

@[simp]

theorem TauCeti.BinaryQuadraticForm.T_smul (f : BinaryQuadraticForm ℤ) : ModularGroup.T • f = { a := f.a, b := f.b - 2 * f.a, c := f.a - f.b + f.c }

The translation T sends a x² + b x y + c y² to a x² + (b - 2 a) x y + (a - b + c) y².

@[simp]

theorem TauCeti.BinaryQuadraticForm.S_smul (f : BinaryQuadraticForm ℤ) : ModularGroup.S • f = { a := f.c, b := -f.b, c := f.a }

The rotation S sends a x² + b x y + c y² to c x² - b x y + a y².

theorem TauCeti.BinaryQuadraticForm.discrim_swap {R : Type u_1} [CommRing R] (f : BinaryQuadraticForm R) : { a := f.c, b := f.b, c := f.a }.discrim = f.discrim

Exchanging the outer coefficients of a x² + b x y + c y² preserves the discriminant.