The splitting criterion for quaternion algebras

Over a field K in which 2 is invertible, a quaternion algebra ℍ[K,a,b] with a, b ∈ Kˣ is either a division algebra or isomorphic to the matrix algebra M₂(K), and which case occurs is decided by quadratic forms. This file proves the classical criterion: the following are equivalent.

1. ℍ[K,a,b] splits, that is ℍ[K,a,b] ≃ₐ[K] Matrix (Fin 2) (Fin 2) K;
2. b is a norm from the quadratic algebra K[√a] = QuadraticAlgebra K a 0;
3. b = x² - a y² for some x, y ∈ K;
4. the ternary form ⟨1, -a, -b⟩ is isotropic;
5. the norm form ⟨1, -a, -b, ab⟩ of ℍ[K,a,b] is isotropic.

No hypothesis that a is a nonsquare is needed: when a is a square the form x² - a y² is universal and all five conditions hold.

The arguments are elementary. A quaternion is invertible exactly when its norm is (QuaternionAlgebra.isUnit_iff_normForm_isUnit), so ℍ[K,a,b] is a division algebra exactly when its norm form is anisotropic (QuaternionAlgebra.anisotropic_normForm_iff); since M₂(K) has nonzero non-invertible elements, a split algebra has an isotropic norm form. An isotropic vector t + u i + v j + w k of the norm form gives t² - a u² = b (v² - a w²), and dividing in K[√a] exhibits b as a norm. Conversely, if b = N(z) then TauCeti.QuaternionAlgebra.normMulEquiv identifies ℍ[K,a,b] with ℍ[K,a,1], which is split by TauCeti.QuaternionAlgebra.oneEquivMatrix.

Main results

• TauCeti.exists_eq_sq_sub_mul_sq_of_isSquare: x² - a y² is universal when a is a square unit.
• TauCeti.sq_sub_mul_sq_eq_zero_iff: over a field, x² - a y² is anisotropic when a is not a square.
• TauCeti.exists_eq_sq_sub_mul_sq_of_not_anisotropic: an isotropic ternary form ⟨1, -a, -b⟩ exhibits b in the form x² - a y².
• TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_tfae: the splitting criterion.
• TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_iff_not_forall_isUnit and TauCeti.QuaternionAlgebra.forall_isUnit_or_nonempty_algEquiv_matrix: ℍ[K,a,b] is split exactly when it is not a division algebra.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter III, Theorems 2.7 and 4.2 (Lam writes ⟨⟨a,b⟩⟩ for the norm form and (a,b) for the algebra).
• J.-P. Serre, A Course in Arithmetic (1973), Chapter III, Proposition 1.
• P. Gille, T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), Proposition 1.1.7 and Corollary 1.1.9.

theorem TauCeti.exists_eq_sq_sub_mul_sq_of_isSquare {R : Type u_1} [CommRing R] [Invertible 2] {a : R} (ha : IsSquare a) (ha' : IsUnit a) (b : R) : ∃ (x : R) (y : R), b = x ^ 2 - a * y ^ 2

The norm form of a split quadratic algebra is universal. If a is the square of a unit, then every b is of the form x² - a y²: explicitly x = (b + 1) / 2 and y = (b - 1) / (2 s) for a = s².

theorem TauCeti.sq_sub_mul_sq_eq_zero_iff {K : Type u_1} [Field K] {a : K} (ha : ¬IsSquare a) {p q : K} : p ^ 2 - a * q ^ 2 = 0 ↔ p = 0 ∧ q = 0

Over a field, p² - a q² vanishes only at p = q = 0 when a is not a square.

theorem TauCeti.exists_eq_sq_sub_mul_sq_of_not_anisotropic {K : Type u_1} [Field K] [Invertible 2] {a b : K} (ha : a ≠ 0) (h : ¬(QuadraticMap.weightedSumSquares K ![1, -a, -b]).Anisotropic) : ∃ (x : K) (y : K), b = x ^ 2 - a * y ^ 2

An isotropic ternary form ⟨1, -a, -b⟩ exhibits b in the form x² - a y².

theorem TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_tfae {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : [Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K), ∃ (z : QuadraticAlgebra K (↑a) 0), QuadraticAlgebra.norm z = ↑b, ∃ (x : K) (y : K), ↑b = x ^ 2 - ↑a * y ^ 2, ¬(QuadraticMap.weightedSumSquares K ![1, -↑a, -↑b]).Anisotropic, ¬QuadraticMap.Anisotropic (QuaternionAlgebra.normForm (↑a) 0 ↑b)].TFAE

The splitting criterion for quaternion algebras (Lam III.2.7 and III.4.2, Serre III.1, Gille-Szamuely 1.1.9). For units a and b of a field in which 2 is invertible, the following are equivalent:

1. ℍ[K,a,b] is isomorphic to M₂(K);
2. b is a norm from K[√a] = QuadraticAlgebra K a 0;
3. b = x² - a y² for some x, y ∈ K;
4. the ternary form ⟨1, -a, -b⟩ is isotropic;
5. the norm form of ℍ[K,a,b], that is ⟨1, -a, -b, ab⟩, is isotropic.

theorem TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_iff_exists_norm_eq {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K) ↔ ∃ (z : QuadraticAlgebra K (↑a) 0), QuadraticAlgebra.norm z = ↑b

ℍ[K,a,b] is split exactly when b is a norm from K[√a].

theorem TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_iff_exists_eq_sq_sub_mul_sq {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K) ↔ ∃ (x : K) (y : K), ↑b = x ^ 2 - ↑a * y ^ 2

ℍ[K,a,b] is split exactly when b = x² - a y² is solvable.

theorem TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_iff_not_anisotropic_weightedSumSquares {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K) ↔ ¬(QuadraticMap.weightedSumSquares K ![1, -↑a, -↑b]).Anisotropic

ℍ[K,a,b] is split exactly when ⟨1, -a, -b⟩ is isotropic.

theorem TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_iff_not_anisotropic_normForm {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K) ↔ ¬QuadraticMap.Anisotropic (QuaternionAlgebra.normForm (↑a) 0 ↑b)

ℍ[K,a,b] is split exactly when its norm form is isotropic.

theorem TauCeti.QuaternionAlgebra.nonempty_algEquiv_matrix_iff_not_forall_isUnit {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K) ↔ ¬∀ (x : QuaternionAlgebra K (↑a) 0 ↑b), x ≠ 0 → IsUnit x

Split or division (Lam III.2.7). ℍ[K,a,b] is split exactly when it is not a division algebra.

theorem TauCeti.QuaternionAlgebra.forall_isUnit_or_nonempty_algEquiv_matrix {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : (∀ (x : QuaternionAlgebra K (↑a) 0 ↑b), x ≠ 0 → IsUnit x) ∨ Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)

Split or division. Every quaternion algebra ℍ[K,a,b] is a division algebra or is isomorphic to M₂(K).