Quaternion algebras attached to binary quadratic forms

The Clifford algebra of the diagonal binary form ⟨a, b⟩ is the quaternion algebra ℍ[R,a,b]. Consequently, an isometry between two binary diagonal forms induces an algebra equivalence between the corresponding quaternion algebras. This is the binary quaternion lemma used to prove that Hasse invariants are independent of a diagonalization.

The result is stated over a commutative ring: Mathlib's Clifford-algebra construction and its quaternion equivalence require neither a field nor invertibility of two.

Main definitions

• TauCeti.QuaternionAlgebra.weightedSumSquaresIsometryEquivQ: the diagonal binary form ⟨w 0, w 1⟩ is isometric to Mathlib's quaternion plane form CliffordAlgebraQuaternion.Q.

Main result

• TauCeti.QuaternionAlgebra.nonempty_algEquiv_of_equivalent_binary: equivalent binary diagonal forms have isomorphic quaternion algebras.

Reference

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter III, §2.11.

def TauCeti.QuaternionAlgebra.weightedSumSquaresIsometryEquivQ {R : Type u} [CommRing R] (w : Fin 2 → R) : (QuadraticMap.weightedSumSquares R w).IsometryEquiv (CliffordAlgebraQuaternion.Q (w 0) (w 1))

The diagonal binary form ⟨w 0, w 1⟩ is isometric to Mathlib's quaternion plane form CliffordAlgebraQuaternion.Q (w 0) (w 1), whose Clifford algebra is ℍ[R, w 0, w 1], through the coordinate identification (Fin 2 → R) ≃ R × R.

Equations

• TauCeti.QuaternionAlgebra.weightedSumSquaresIsometryEquivQ w = { toLinearEquiv := LinearEquiv.finTwoArrow R R, map_app' := ⋯ }

theorem TauCeti.QuaternionAlgebra.nonempty_algEquiv_of_equivalent_binary {R : Type u} [CommRing R] (a b c d : R) (h : (QuadraticMap.weightedSumSquares R ![a, b]).Equivalent (QuadraticMap.weightedSumSquares R ![c, d])) : Nonempty (QuaternionAlgebra R a 0 b ≃ₐ[R] QuaternionAlgebra R c 0 d)

The binary quaternion lemma. If the diagonal binary forms ⟨a, b⟩ and ⟨c, d⟩ are equivalent, then the quaternion algebras ℍ[R,a,b] and ℍ[R,c,d] are isomorphic as R-algebras.

This follows by functoriality of Clifford algebras under isometries and Mathlib's identification of the Clifford algebra of a binary diagonal form with the corresponding quaternion algebra.