Proper automorphisms of binary lattices and norm-one units

Let L be an integral lattice of rank two with nonzero form, and fix a carrier basis. Writing a proper isometry of L as its matrix in that basis identifies SO(L) with the stabilizer in SL(2, ℤ) of the binary norm form, that is, with its proper automorphs (TauCeti.IntegralLattice.specialOrthogonalGroupEquivStabilizer). Through the primitive part of the norm form, these are the norm-one units of the quadratic order 𝒪(L) = ℤ[(Δ + √Δ)/2] of the primitive discriminant Δ:

SO(L) ≃* {u ∈ 𝒪(L)ˣ : N(u) = 1}.

The unit x + y√Δ acts by !![x - b y, -2 c y; 2 a y, x + b y], where (a, b, c) is the primitive part of the norm form. The isomorphism depends on the basis only through conjugation, and it holds for degenerate nonzero forms as well.

The three cases of the unit group give the size of SO(L):

• for Δ < 0, every unit has norm one, so |SO(L)| = #𝒪(L)ˣ, which is 6, 4 or 2;
• for Δ > 0 not a square, Pell's equation gives infinitely many norm-one units, so SO(L) and O(L) are infinite;
• for a nonzero square Δ, the norm-one units are ±1, so SO(L) = {±1}.

The infinite case is the input that the anisotropic indefinite lattices of rank at least three need, since their automorphisms are built from those of an anisotropic binary sublattice.

Main results

• TauCeti.IntegralLattice.specialOrthogonalGroupEquivNormOneUnits: SO(L) is the group of norm-one units of the order of L.
• TauCeti.IntegralLattice.card_specialOrthogonalGroup_of_binaryDiscriminant_neg: for negative discriminant, |SO(L)| = #𝒪(L)ˣ.
• TauCeti.IntegralLattice.infinite_isometry_of_binaryDiscriminant_pos_of_not_isSquare: for positive nonsquare discriminant, O(L) is infinite, and already SO(L) is, by infinite_specialOrthogonalGroup_of_binaryDiscriminant_pos_of_not_isSquare.
• TauCeti.IntegralLattice.card_specialOrthogonalGroup_of_isSquare_binaryDiscriminant: for a nonzero square discriminant, |SO(L)| = 2.

References

• D. A. Cox, Primes of the Form x² + ny², §2 and §7.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 13.

noncomputable def TauCeti.IntegralLattice.specialOrthogonalGroupEquivNormOneUnits {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (hV : Module.finrank ℚ V = 2) (hL : L.form ≠ 0) : ↥L.specialOrthogonalGroup ≃* ↥(QuadraticOrder.normOneUnits (L.binaryDiscriminant hV) ⋯)

Proper isometries of a binary lattice are norm-one units. For a rank-two lattice with nonzero form and a carrier basis b, the proper isometries form a group isomorphic to the norm-one units of the quadratic order of the primitive discriminant. The inverse is described by map_toMatrix_specialOrthogonalGroupEquivNormOneUnits_symm_apply.

theorem TauCeti.IntegralLattice.map_toMatrix_specialOrthogonalGroupEquivNormOneUnits_symm_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (hV : Module.finrank ℚ V = 2) (hL : L.form ≠ 0) (u : ↥(QuadraticOrder.normOneUnits (L.binaryDiscriminant hV) ⋯)) : ((LinearMap.toMatrix b b) ↑(↑((specialOrthogonalGroupEquivNormOneUnits b hV hL).symm u)).carrierEquiv).map Int.cast = have f := (L.binaryNormForm b).primPart; have O := QuadraticOrder.toSubalgebra (L.binaryDiscriminant hV) ⋯; 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 proper isometry attached to the norm-one unit x + y√Δ has matrix !![x - b y, -2 c y; 2 a y, x + b y] in the carrier basis, read over ℚ, where (a, b, c) is the primitive part of the norm form.

theorem TauCeti.IntegralLattice.card_specialOrthogonalGroup_of_binaryDiscriminant_neg {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hV : Module.finrank ℚ V = 2) (hneg : L.binaryDiscriminant hV < 0) : Nat.card ↥L.specialOrthogonalGroup = Nat.card (↥(L.binaryOrder hV))ˣ

Negative discriminant. For a rank-two lattice of negative primitive discriminant, the proper isometries are as many as the units of its quadratic order. The unit count is QuadraticOrder.card_units_of_neg: 6 for Δ = -3, 4 for Δ = -4, and 2 otherwise.

theorem TauCeti.IntegralLattice.infinite_specialOrthogonalGroup_of_binaryDiscriminant_pos_of_not_isSquare {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hV : Module.finrank ℚ V = 2) (hpos : 0 < L.binaryDiscriminant hV) (hns : ¬IsSquare (L.binaryDiscriminant hV)) : Infinite ↥L.specialOrthogonalGroup

Positive nonsquare discriminant. A rank-two lattice whose primitive discriminant is positive and not a square has infinitely many proper isometries, by Pell's equation.

theorem TauCeti.IntegralLattice.infinite_isometry_of_binaryDiscriminant_pos_of_not_isSquare {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hV : Module.finrank ℚ V = 2) (hpos : 0 < L.binaryDiscriminant hV) (hns : ¬IsSquare (L.binaryDiscriminant hV)) : Infinite (L.Isometry L)

Positive nonsquare discriminant. A rank-two lattice whose primitive discriminant is positive and not a square has infinitely many isometries.

theorem TauCeti.IntegralLattice.card_specialOrthogonalGroup_of_isSquare_binaryDiscriminant {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hV : Module.finrank ℚ V = 2) (hsq : IsSquare (L.binaryDiscriminant hV)) (h₀ : L.binaryDiscriminant hV ≠ 0) : Nat.card ↥L.specialOrthogonalGroup = 2

Nonzero square discriminant. A rank-two lattice whose primitive discriminant is a nonzero square has exactly two proper isometries, the identity and negation.