Norm-one units of quadratic orders

The norm-one subgroup is the kernel of the ordinary algebra norm on the units of the embedded quadratic order. The existing integral quadratic-algebra model identifies this subgroup with its unitary elements. This comparison supplies integral coordinates for the unit arithmetic used by binary lattice automorphisms.

At negative discriminant every unit has norm one, with six units at minus three, four at minus four, and two otherwise. At positive nonsquare discriminant the embedded Pell solutions give infinitely many norm-one units. At nonzero square discriminant the product-order norm calculation leaves exactly the diagonal units one and minus one.

References

• D. A. Cox, Primes of the Form x² + ny², Sections 2 and 7.

noncomputable def TauCeti.QuadraticOrder.normOneUnits (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Subgroup (↥(toSubalgebra D hD))ˣ

The norm-one subgroup of the units of the embedded quadratic order.

@[simp]

theorem TauCeti.QuadraticOrder.mem_normOneUnits_iff (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (u : (↥(toSubalgebra D hD))ˣ) : u ∈ normOneUnits D hD ↔ (Algebra.norm ℤ) ↑u = 1

A unit lies in the norm-one subgroup exactly when its ordinary algebra norm equals one.

@[simp]

theorem TauCeti.QuadraticOrder.norm_equivToSubalgebra (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (z : QuadraticAlgebra ℤ ((D - D ^ 2) / 4) D) : (Algebra.norm ℤ) ((equivToSubalgebra D hD) z) = QuadraticAlgebra.norm z

The integral-model equivalence identifies the algebra norm with the quadratic norm.

noncomputable def TauCeti.QuadraticOrder.normOneUnitsEquivUnitary (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : ↥(normOneUnits D hD) ≃* ↥(unitary (QuadraticAlgebra ℤ ((D - D ^ 2) / 4) D))

Norm-one units of the actual embedded order are the unitary elements of its integral model.

@[simp]

theorem TauCeti.QuadraticOrder.coe_normOneUnitsEquivUnitary_symm (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (z : ↥(unitary (QuadraticAlgebra ℤ ((D - D ^ 2) / 4) D))) : ↑↑((normOneUnitsEquivUnitary D hD).symm z) = (equivToSubalgebra D hD) ↑z

The inverse comparison embeds a unitary integral-model element in the actual order.

@[simp]

theorem TauCeti.QuadraticOrder.coe_normOneUnitsEquivUnitary_apply (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (u : ↥(normOneUnits D hD)) : ↑((normOneUnitsEquivUnitary D hD) u) = (equivToSubalgebra D hD).symm ↑↑u

The forward comparison recovers the integral coordinates of the underlying order element.

theorem TauCeti.QuadraticOrder.norm_coe (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (z : ↥(toSubalgebra D hD)) : QuadraticAlgebra.norm ↑z = ↑((Algebra.norm ℤ) z)

The norm in the rational quadratic algebra is the integer norm of the embedded order.

theorem TauCeti.QuadraticOrder.norm_unit_eq_one_of_neg (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (hneg : D < 0) (u : (↥(toSubalgebra D hD))ˣ) : (Algebra.norm ℤ) ↑u = 1

For negative discriminant every unit has norm one.

theorem TauCeti.QuadraticOrder.normOneUnits_eq_top_of_neg (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (hneg : D < 0) : normOneUnits D hD = ⊤

At negative discriminant the norm-one subgroup is the full unit group.

theorem TauCeti.QuadraticOrder.neg_one_mem_normOneUnits (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : -1 ∈ normOneUnits D hD

Minus one is a norm-one unit of every quadratic order.

theorem TauCeti.QuadraticOrder.units_eq_one_or_neg_one_of_neg (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (hneg : D < 0) (h₃ : D ≠ -3) (h₄ : D ≠ -4) (u : (↥(toSubalgebra D hD))ˣ) : u = 1 ∨ u = -1

Away from discriminants minus three and minus four, a negative-discriminant order has only the units one and minus one.

theorem TauCeti.QuadraticOrder.card_units_of_neg_of_ne (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (hneg : D < 0) (h₃ : D ≠ -3) (h₄ : D ≠ -4) : Nat.card (↥(toSubalgebra D hD))ˣ = 2

Apart from the two exceptional negative discriminants, the unit group has order two.

theorem TauCeti.QuadraticOrder.card_units_neg_four : Nat.card (↥(toSubalgebra (-4) card_units_neg_four._proof_1))ˣ = 4

The discriminant-minus-four order has four units.

theorem TauCeti.QuadraticOrder.card_units_neg_three : Nat.card (↥(toSubalgebra (-3) card_units_neg_three._proof_1))ˣ = 6

The discriminant-minus-three order has six units.

theorem TauCeti.QuadraticOrder.card_units_of_neg (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (hneg : D < 0) : Nat.card (↥(toSubalgebra D hD))ˣ = if D = -3 then 6 else if D = -4 then 4 else 2

The unit count for every negative quadratic discriminant, including the two exceptions.

theorem TauCeti.QuadraticOrder.card_normOneUnits_of_neg (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (hneg : D < 0) : Nat.card ↥(normOneUnits D hD) = if D = -3 then 6 else if D = -4 then 4 else 2

The norm-one unit count at negative discriminant.

theorem TauCeti.QuadraticOrder.finite_normOneUnits_of_neg (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (hneg : D < 0) : Finite ↥(normOneUnits D hD)

Negative-discriminant quadratic orders have finite norm-one unit groups.

theorem TauCeti.QuadraticOrder.norm_eq_product_of_sq (s : ℤ) (hs : s ≠ 0) (z : ↥(toSubalgebra (s ^ 2) ⋯)) : (Algebra.norm ℤ) z = (↑((equivProductOfSq s hs) z)).1 * (↑((equivProductOfSq s hs) z)).2

In the split branch, the integer norm is multiplication of the product coordinates.

theorem TauCeti.QuadraticOrder.normOneUnits_eq_one_or_neg_one_of_sq (s : ℤ) (hs : s ≠ 0) (u : ↥(normOneUnits (s ^ 2) ⋯)) : ↑u = 1 ∨ ↑u = -1

The norm-one units of a nonzero square-discriminant order are precisely one and minus one.

theorem TauCeti.QuadraticOrder.card_normOneUnits_sq (s : ℤ) (hs : s ≠ 0) : Nat.card ↥(normOneUnits (s ^ 2) ⋯) = 2

A nonzero square-discriminant order has two norm-one units, computed in the product order.

theorem TauCeti.QuadraticOrder.finite_normOneUnits_sq (s : ℤ) (hs : s ≠ 0) : Finite ↥(normOneUnits (s ^ 2) ⋯)

Nonzero square-discriminant quadratic orders have finite norm-one unit groups.

noncomputable def TauCeti.QuadraticOrder.pellToNormOneUnits (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Pell.Solution₁ D →* ↥(normOneUnits D hD)

An ordinary Pell solution gives a norm-one unit of the actual quadratic order.

@[simp]

theorem TauCeti.QuadraticOrder.coe_pellToNormOneUnits (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (a : Pell.Solution₁ D) : ↑↑↑((pellToNormOneUnits D hD) a) = { re := ↑a.x, im := ↑a.y }

The embedded unit attached to (x, y) is exactly x + y√D.

theorem TauCeti.QuadraticOrder.pellToNormOneUnits_injective (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Function.Injective ⇑(pellToNormOneUnits D hD)

Distinct Pell solutions give distinct units in the order.

theorem TauCeti.QuadraticOrder.infinite_normOneUnits_of_pos_of_not_isSquare (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (hpos : 0 < D) (hns : ¬IsSquare D) : Infinite ↥(normOneUnits D hD)

Positive nonsquare discriminants have infinitely many integral norm-one units, by powers of a fundamental Pell solution.