Isotropic two-fold Pfister forms are hyperbolic

For units a, b of a field K in which 2 is invertible, the two-fold Pfister form <<a, b>> = <1, -a, -b, ab> is the norm form of the quaternion algebra ℍ[K,a,b]. This file proves that the following are equivalent:

1. ℍ[K,a,b] is split, that is isomorphic to M₂(K);
2. <<a, b>> is isotropic;
3. <<a, b>> is hyperbolic, that is isometric to the sum of two hyperbolic planes;
4. the Witt class of <<a, b>> vanishes.

The equivalence of (2) and (3), that an isotropic two-fold Pfister form is hyperbolic, is the first case of the theorem that isotropic Pfister forms are hyperbolic. The equivalence of (1) and (4) says that the Witt class of <<a, b>> detects whether ℍ[K,a,b] is split.

Main results

• TauCeti.anisotropic_pfisterFormClass_two_iff: <<a, b>> is anisotropic exactly when the norm form of ℍ[K,a,b] is.
• TauCeti.pfisterFormClass_two_tfae: the four conditions above are equivalent, with the individual equivalences TauCeti.not_anisotropic_pfisterFormClass_two_iff, TauCeti.pfisterFormClass_two_eq_two_nsmul_hyperbolicClass_iff and TauCeti.pfisterClass_two_eq_zero_iff.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter III, §2 (the splitting criterion, Theorem 2.7) and Chapter X, §1 (isotropic Pfister forms are hyperbolic), with the convention <<a>> = <1, -a>.

theorem TauCeti.anisotropic_pfisterFormClass_two_iff {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : (pfisterFormClass ![a, b]).Anisotropic ↔ QuadraticMap.Anisotropic (QuaternionAlgebra.normForm (↑a) 0 ↑b)

The two-fold Pfister form <<a, b>> is anisotropic exactly when the norm form of the quaternion algebra ℍ[K,a,b] is.

theorem TauCeti.not_anisotropic_pfisterFormClass_two_iff {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : ¬(pfisterFormClass ![a, b]).Anisotropic ↔ pfisterFormClass ![a, b] = 2 • hyperbolicClass K

A two-fold Pfister form is isotropic exactly when it is hyperbolic.

theorem TauCeti.pfisterFormClass_two_tfae {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : [Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K), ¬(pfisterFormClass ![a, b]).Anisotropic, pfisterFormClass ![a, b] = 2 • hyperbolicClass K, pfisterClass ![a, b] = 0].TFAE

Isotropy, hyperbolicity and splitting for two-fold Pfister forms. For units a, b, the following are equivalent:

1. ℍ[K,a,b] is isomorphic to M₂(K);
2. <<a, b>> is isotropic;
3. <<a, b>> is the sum of two hyperbolic planes;
4. the Witt class of <<a, b>> vanishes.

theorem TauCeti.pfisterFormClass_two_eq_two_nsmul_hyperbolicClass_iff {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : pfisterFormClass ![a, b] = 2 • hyperbolicClass K ↔ Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)

Hyperbolicity criterion for two-fold Pfister forms: the regular form class of <<a, b>> is the sum of two hyperbolic planes exactly when ℍ[K,a,b] is split.

theorem TauCeti.pfisterClass_two_eq_zero_iff {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : pfisterClass ![a, b] = 0 ↔ Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)

The Witt class of the two-fold Pfister form <<a, b>> vanishes exactly when ℍ[K,a,b] is split.