Splitting of quaternion algebras

TheoremAnisotropy of the quaternion norm form reduces to a ternary form#✓fully proved

The quaternary norm form x₀² - a·x₁² - b·x₂² + a·b·x₃² of the quaternion algebra ℍ[K, a, b] is anisotropic if and only if the ternary form z² - a·x² - b·y² is. This equivalence also holds when either parameter is zero; both forms are then isotropic.

This is the standard reduction of quaternion-algebra isotropy to a ternary quadratic form. It is used to test whether a quaternion algebra is a division algebra, in quadratic-form theory (anisotropy of Pfister forms), and in local-global arguments for quaternion algebras.

theorem forall_quaternary_normForm_eq_zero_iff_forall_ternary_eq_zero (K : Type)
    [Field K] (a b : K) :
    (∀ x₀ x₁ x₂ x₃ : K, x₀ ^ 2 - a * x₁ ^ 2 - b * x₂ ^ 2 + a * b * x₃ ^ 2 = 0 →
        x₀ = 0 ∧ x₁ = 0 ∧ x₂ = 0 ∧ x₃ = 0) ↔
      ∀ z x y : K, z ^ 2 - a * x ^ 2 - b * y ^ 2 = 0 → z = 0 ∧ x = 0 ∧ y = 0

TheoremQuaternion algebras with isotropic norm form split#✓fully proved

If the norm form of a quaternion algebra over a field of characteristic not two is isotropic, then the algebra splits: it is isomorphic to the 2 × 2 matrix algebra.

theorem nonempty_algEquiv_matrix_of_normForm_eq_zero
    (K : Type) [Field K] (h2 : (2 : K) ≠ 0) (a b : K) (ha : a ≠ 0) (hb : b ≠ 0)
    (x₀ x₁ x₂ x₃ : K) (hx : ¬ (x₀ = 0 ∧ x₁ = 0 ∧ x₂ = 0 ∧ x₃ = 0))
    (h0 : x₀ ^ 2 - a * x₁ ^ 2 - b * x₂ ^ 2 + a * b * x₃ ^ 2 = 0) :
    Nonempty (ℍ[K, a, b] ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.