Automorphs of a binary quadratic form and norm-one units

The stabilizer of an integral binary quadratic form f = (a, b, c) in SL(2, ℤ) is its group of proper automorphs. For primitive f of discriminant D = b² - 4ac it is isomorphic to the group of norm-one units of the quadratic order 𝒪_D = ℤ[(D + √D)/2] of discriminant D. The unit x + y√D corresponds to the automorph

!![x - b y, -2 c y; 2 a y, x + b y],

classically written !![(t - b u)/2, -c u; a u, (t + b u)/2] with t² - D u² = 4. The assignment is the regular representation of the order on ℤ²: the generator (D + √D)/2 acts by the integral matrix M = !![(D - b)/2, -c; a, (D + b)/2] of trace D, which satisfies M² = (D - D²)/4 + D M and whose form Q_M (TauCeti.BinaryQuadraticForm.ofMatrix) is f. The determinant of the representation is the norm. Matrices commuting with M fix Q_M = f; conversely an automorph of f commutes with M, because Q_M and the trace determine M, and primitivity of f makes its coordinates against M integral.

The same argument works with coefficients in any commutative ring R in which 2 is not a zero divisor, such as ℤ_p, ℚ_p, ℝ or ℚ, for every form whose coefficients a, b, c generate the unit ideal of R. This holds for every primitive form, over a field of characteristic zero for every nonzero form (such as the non-primitive 2 x² + 2 y² over ℚ), and over ℤ_p for every form whose content is prime to p; over ℤ it is primitivity. Reading f over R, its automorphs in SL(2, R) are the norm-one elements of R ⊗ 𝒪_D, in the integral model R[ω]/(ω² - D ω + (D² - D)/4) of 𝒪_D with coefficients in R. This is the group of R-points of the norm-one group scheme of 𝒪_D. This group scheme is a torus over R only when D is invertible in R: for f = x², of discriminant 0, it is μ₂ × 𝔾ₐ over ℚ. The identification is natural in R: a ring homomorphism R →+* S maps automorphs entrywise exactly as it maps the coordinates of norm-one elements. The hypothesis on 2 cannot be dropped: over 𝔽₂ the coordinate swap is an automorph of x y of determinant one, but x y corresponds to the order 𝔽₂ × 𝔽₂, whose only norm-one element is 1.

The isomorphism holds for all such forms, including those of square or zero discriminant. The discriminant is a parameter D with a proof of f.discrim = D, so that the target needs no transport along an equality of discriminants.

Main results

• TauCeti.BinaryQuadraticForm.stabilizerEquivUnitary: for f of discriminant D whose coefficients generate the unit ideal of R, and R without 2-torsion, the automorphs of f over R are the norm-one elements of the order of discriminant D with coefficients in R.
• TauCeti.BinaryQuadraticForm.coe_stabilizerEquivUnitary_symm_apply: the automorph attached to a norm-one element x + y ω.
• TauCeti.BinaryQuadraticForm.map_stabilizerEquivUnitary_symm_apply: naturality in the coefficient ring.
• TauCeti.BinaryQuadraticForm.stabilizerEquivNormOneUnits: over ℤ, the automorphs of f are the norm-one units of the order of discriminant D.
• TauCeti.BinaryQuadraticForm.map_stabilizerEquivNormOneUnits_symm_apply: the automorph attached to the unit x + y√D.

References

• D. A. Cox, Primes of the Form x² + ny², §2 and §7.
• L. E. Dickson, Introduction to the Theory of Numbers, Chapter VII.

The integral generator matrix

The regular representation over a coefficient ring

Automorphs and norm-one elements over a coefficient ring

noncomputable def TauCeti.BinaryQuadraticForm.stabilizerEquivUnitary {R : Type u_1} [CommRing R] {f : BinaryQuadraticForm ℤ} {D : ℤ} (hf : Ideal.span {↑f.a, ↑f.b, ↑f.c} = ⊤) (hfD : f.discrim = D) (h2 : IsLeftRegular 2) : ↥(MulAction.stabilizer (Matrix.SpecialLinearGroup (Fin 2) R) (map (Int.castRingHom R) f)) ≃* ↥(unitary (QuadraticAlgebra R ↑((D - D ^ 2) / 4) ↑D))

Automorphs are norm-one elements of the order. Let f be an integral binary quadratic form of discriminant D, and let R be a commutative ring in which 2 is not a zero divisor and the coefficients a, b, c of f generate the unit ideal, for instance any R when f is primitive (IsPrimitive.span_intCast_eq_top). The proper automorphs of f with coefficients in R form a group isomorphic to the norm-one elements of R[ω]/(ω² - D ω + (D² - D)/4), the quadratic order ℤ[(D + √D)/2] of discriminant D with coefficients in R. The inverse is described by coe_stabilizerEquivUnitary_symm_apply.

theorem TauCeti.BinaryQuadraticForm.coe_stabilizerEquivUnitary_symm_apply {R : Type u_1} [CommRing R] {f : BinaryQuadraticForm ℤ} {D : ℤ} (hf : Ideal.span {↑f.a, ↑f.b, ↑f.c} = ⊤) (hfD : f.discrim = D) (h2 : IsLeftRegular 2) (z : ↥(unitary (QuadraticAlgebra R ↑((D - D ^ 2) / 4) ↑D))) : ↑↑((stabilizerEquivUnitary hf hfD h2).symm z) = have x := (↑z).re; have y := (↑z).im; !![x + y * ↑((D - f.b) / 2), -↑f.c * y; ↑f.a * y, x + y * ↑((D + f.b) / 2)]

The automorph attached to the norm-one element x + y ω, where ω is the image of (D + √D)/2, is !![x + y (D - b)/2, -c y; a y, x + y (D + b)/2].

theorem TauCeti.BinaryQuadraticForm.map_stabilizerEquivUnitary_symm_apply {R : Type u_1} [CommRing R] {f : BinaryQuadraticForm ℤ} {D : ℤ} {S : Type u_2} [CommRing S] (φ : R →+* S) (hf : Ideal.span {↑f.a, ↑f.b, ↑f.c} = ⊤) (hfD : f.discrim = D) (hR : IsLeftRegular 2) (hS : IsLeftRegular 2) (z : ↥(unitary (QuadraticAlgebra R ↑((D - D ^ 2) / 4) ↑D))) (w : ↥(unitary (QuadraticAlgebra S ↑((D - D ^ 2) / 4) ↑D))) (hre : (↑w).re = φ (↑z).re) (him : (↑w).im = φ (↑z).im) : (Matrix.SpecialLinearGroup.map φ) ↑((stabilizerEquivUnitary hf hfD hR).symm z) = ↑((stabilizerEquivUnitary ⋯ hfD hS).symm w)

Naturality in the coefficient ring. A ring homomorphism φ : R →+* S maps the automorph attached to a norm-one element z over R entrywise to the automorph attached to the norm-one element over S whose coordinates are the images of those of z.

Integral automorphs and norm-one units

noncomputable def TauCeti.BinaryQuadraticForm.stabilizerEquivNormOneUnits {f : BinaryQuadraticForm ℤ} {D : ℤ} (hf : f.IsPrimitive) (hfD : f.discrim = D) : ↥(MulAction.stabilizer (Matrix.SpecialLinearGroup (Fin 2) ℤ) f) ≃* ↥(QuadraticOrder.normOneUnits D ⋯)

Automorphs are norm-one units. For a primitive integral binary quadratic form f of discriminant D, the proper automorphs of f form a group isomorphic to the norm-one units of the quadratic order ℤ[(D + √D)/2] of discriminant D. This is the case R = ℤ of stabilizerEquivUnitary, read in the embedded order. The inverse is described by map_stabilizerEquivNormOneUnits_symm_apply.

theorem TauCeti.BinaryQuadraticForm.map_stabilizerEquivNormOneUnits_symm_apply {f : BinaryQuadraticForm ℤ} {D : ℤ} (hf : f.IsPrimitive) (hfD : f.discrim = D) (u : ↥(QuadraticOrder.normOneUnits D ⋯)) : (↑↑((stabilizerEquivNormOneUnits hf hfD).symm u)).map Int.cast = have O := QuadraticOrder.toSubalgebra D ⋯; have x := (↑↑↑u).re; have y := (↑↑↑u).im; !![x - ↑f.b * y, -2 * ↑f.c * y; 2 * ↑f.a * y, x + ↑f.b * y]

The automorph attached to the norm-one unit x + y√D of the order is !![x - b y, -2 c y; 2 a y, x + b y], read over ℚ.