Square-discriminant quadratic orders

For a nonzero integer s, the canonical order of discriminant s² is isomorphic to {(x, y) : ℤ × ℤ | s ∣ x - y}. The isomorphism agrees with the rational splitting at the two roots s and -s, so it identifies the actual embedded orders.

This transfers the congruence product order's unit count to the canonical order. At discriminant one the order is the full integer product, with four units.

References

• D. A. Cox, Primes of the Form x² + ny², §7.

noncomputable def TauCeti.QuadraticOrder.equivProductOfSq (s : ℤ) (hs : s ≠ 0) : ↥(toSubalgebra (s ^ 2) ⋯) ≃ₐ[ℤ] ↥(productSubalgebra s)

The canonical order of nonzero square discriminant is the integer congruence product order.

noncomputable def TauCeti.QuadraticOrder.algEquivProdOfIntSq (s : ℤ) (hs : s ≠ 0) : QuadraticAlgebra ℚ (↑(s ^ 2)) 0 ≃ₐ[ℚ] ℚ × ℚ

The rational quadratic algebra of a nonzero integer square splits at its two roots.

@[simp]

theorem TauCeti.QuadraticOrder.algEquivProdOfIntSq_apply (s : ℤ) (hs : s ≠ 0) (z : QuadraticAlgebra ℚ (↑(s ^ 2)) 0) : (algEquivProdOfIntSq s hs) z = (z.re + ↑s * z.im, z.re - ↑s * z.im)

The rational splitting evaluates at the opposite integer roots.

@[simp]

theorem TauCeti.QuadraticOrder.coe_equivProductOfSq_apply (s : ℤ) (hs : s ≠ 0) (z : QuadraticAlgebra ℤ ((s ^ 2 - (s ^ 2) ^ 2) / 4) (s ^ 2)) : ↑((equivProductOfSq s hs) ((equivToSubalgebra (s ^ 2) ⋯) z)) = (z.re + ((s ^ 2 - s) / 2 + s) * z.im, z.re + (s ^ 2 - s) / 2 * z.im)

The order isomorphism evaluates the shifted integral generator in both coordinates.

theorem TauCeti.QuadraticOrder.equivProductOfSq_commutes (s : ℤ) (hs : s ≠ 0) (z : ↥(toSubalgebra (s ^ 2) ⋯)) : (algEquivProdOfIntSq s hs) ↑z = (↑(↑((equivProductOfSq s hs) z)).1, ↑(↑((equivProductOfSq s hs) z)).2)

The order isomorphism agrees with the rational splitting on its embedded elements.

theorem TauCeti.QuadraticOrder.map_toSubalgebra_of_sq (s : ℤ) (hs : s ≠ 0) : Subalgebra.map (AlgHom.restrictScalars ℤ ↑(algEquivProdOfIntSq s hs)) (toSubalgebra (s ^ 2) ⋯) = Subalgebra.map ((Algebra.ofId ℤ ℚ).prodMap (Algebra.ofId ℤ ℚ)) (productSubalgebra s)

The rational splitting identifies the embedded canonical order with the embedded congruence product order.

theorem TauCeti.QuadraticOrder.card_units_toSubalgebra_sq (s : ℤ) (hs : s ≠ 0) : Nat.card (↥(toSubalgebra (s ^ 2) ⋯))ˣ = if s ∣ 2 then 4 else 2

The unit group of the square-discriminant order has cardinality four when s ∣ 2, and two otherwise.

noncomputable def TauCeti.QuadraticOrder.equivProdOfOne : ↥(toSubalgebra 1 equivProdOfOne._proof_1) ≃ₐ[ℤ] ℤ × ℤ

At discriminant one the canonical order is the full integer product.

@[simp]

theorem TauCeti.QuadraticOrder.coe_equivProdOfOne_apply (z : ↥(toSubalgebra 1 equivProdOfOne._proof_1)) : (↑(equivProdOfOne z).1, ↑(equivProdOfOne z).2) = ((↑z).re + (↑z).im, (↑z).re - (↑z).im)

The rational coordinates of the discriminant-one order equivalence evaluate at both roots.

theorem TauCeti.QuadraticOrder.card_units_toSubalgebra_one : Nat.card (↥(toSubalgebra 1 equivProdOfOne._proof_1))ˣ = 4

The discriminant-one order has four units.