Two dyadic phenomena for bilinear forms

The hyperbolic plane over ℤ_[2], obtained from the integer Gram matrix !![0, 1; 1, 0], has no orthogonal basis. It illustrates why diagonalization of integral bilinear forms over ℤ_[p] requires the prime p to be odd.

Odd unimodular forms over ℤ_[2] do have orthogonal bases, but unlike at odd primes their rank and determinant square class do not classify them: the oddity, the trace of a diagonal Gram matrix modulo 8, is a further invariant. The forms ⟨1, 1⟩ and ⟨3, 3⟩ are separated by it.

Main results

• TauCeti.not_exists_orthogonal_basis_hyperbolic_padicInt_two: the hyperbolic plane over ℤ_[2] has no orthogonal basis.
• TauCeti.not_equivalent_toBilin'_diagonal_one_one_three_three_padicInt_two: the forms ⟨1, 1⟩ and ⟨3, 3⟩ over ℤ_[2] are not isometric.

theorem TauCeti.not_exists_orthogonal_basis_hyperbolic_padicInt_two : ¬∃ (b : Module.Basis (Fin 2) ℤ_[2] (Fin 2 → ℤ_[2])), (Matrix.toBilin' (!![0, 1; 1, 0].map Int.cast)).iIsOrtho ⇑b

The dyadic trap. The hyperbolic plane over ℤ_[2] has no orthogonal basis.

theorem TauCeti.not_equivalent_toBilin'_diagonal_one_one_three_three_padicInt_two : ¬(Matrix.toBilin' (Matrix.diagonal ![1, 1])).Equivalent (Matrix.toBilin' (Matrix.diagonal ![3, 3]))

The determinant does not classify odd unimodular forms over ℤ_[2]. The diagonal forms ⟨1, 1⟩ and ⟨3, 3⟩ have the same rank and the square determinants 1 and 9, but they are not isometric: their oddities, the traces 2 and 6 of their Gram matrices, differ modulo 8.