Binary quadratic forms over rings of integers modulo a power of two

This file supplies the elementary normal form used for binary quadratic forms over ℤ/2^{k+1} whose middle coefficient is a unit. Such a form is equivalent either to the hyperbolic form mn or to the form m² + mn + n², by an invertible change of coordinates.

The key input is that, for a unit u, the map s ↦ 2cs² + us is a bijection. Its difference quotient is 2c(s + t) + u, which is a unit because 2 is nilpotent in ℤ/2^{k+1}.

Main results

• ZMod.two_mul_sq_add_bijective: s ↦ 2cs² + us is bijective when u is a unit.
• ZMod.BinaryQuadraticForm.exists_basis: a binary form with unit middle coefficient has one of the two standard normal forms in a basis of (ℤ/2^{k+1})².

theorem ZMod.two_mul_sq_add_bijective {k : ℕ} {c u : ZMod (2 ^ (k + 1))} (hu : IsUnit u) : Function.Bijective fun (s : ZMod (2 ^ (k + 1))) => 2 * c * s ^ 2 + u * s

For a unit u, the map s ↦ 2cs² + us is a bijection of ℤ/2^{k+1}.

theorem ZMod.BinaryQuadraticForm.exists_basis {k : ℕ} (a b : ZMod (2 ^ (k + 1))) {u : ZMod (2 ^ (k + 1))} (hu : IsUnit u) : ∃ (e₁ : ZMod (2 ^ (k + 1))) (e₂ : ZMod (2 ^ (k + 1))) (f₁ : ZMod (2 ^ (k + 1))) (f₂ : ZMod (2 ^ (k + 1))), IsUnit (e₁ * f₂ - f₁ * e₂) ∧ ((∀ (m n : ZMod (2 ^ (k + 1))), a * (m * e₁ + n * f₁) ^ 2 + u * (m * e₁ + n * f₁) * (m * e₂ + n * f₂) + b * (m * e₂ + n * f₂) ^ 2 = m * n) ∨ ∀ (m n : ZMod (2 ^ (k + 1))), a * (m * e₁ + n * f₁) ^ 2 + u * (m * e₁ + n * f₁) * (m * e₂ + n * f₂) + b * (m * e₂ + n * f₂) ^ 2 = m ^ 2 + m * n + n ^ 2)

Normal forms of binary forms with unit middle coefficient over ℤ/2^{k+1}. There is a change of coordinates (m, n) ↦ (me₁ + nf₁, me₂ + nf₂) with unit determinant e₁f₂ - f₁e₂ under which the form am² + umn + bn² becomes mn or m² + mn + n².