Brauer classes of quaternion symbols

For a field K with 2 invertible, this file bundles the quaternion symbol with unit parameters a b : Kˣ as a central simple algebra and defines its Brauer class [(a,b)], the quaternion symbol in BrauerGroup K. The general centrality and simplicity results used here are in TauCeti.Algebra.Quaternion.CentralSimple.

The symbol satisfies the classical relations (Lam III.2.11, Gille–Szamuely 1.5.2):

• it is symmetric, [(a,b)] = [(b,a)], and invariant under multiplying either argument by a square, so it factors through square classes; these follow from isomorphisms of quaternion algebras through TauCeti.BrauerGroup.mk_eq_mk_of_algEquiv;
• it is 2-torsion, [(a,b)]² = 1, because quaternion conjugation identifies ℍ[K,a,b] with its opposite algebra, which TauCeti.BrauerGroup.inv_mk_eq_mk_of_algEquiv_op turns into [(a,b)]⁻¹ = [(a,b)];
• it vanishes on (1,b), (a,-a) and on the Steinberg pair (a,1-a), whose quaternion algebras are isomorphic to M₂(K), and hence by square-class invariance on (a,b²) and (a²,b);
• it is bilinear, [(a,bc)] = [(a,b)] · [(a,c)], from the common slot equivalence ℍ[K,a,b] ⊗[K] ℍ[K,a,c] ≃ₐ[K] ℍ[K,a,bc] ⊗[K] M₂(K) of TauCeti.QuaternionAlgebra.tensorAlgEquivTensorMatrix, read in the Brauer group through the tensor product of central simple algebras;
• it is invariant under isometry of the binary form ⟨a,b⟩, from the binary quaternion lemma.

Equality of two symbols is exactly an isomorphism of the underlying quaternion algebras, and a symbol is trivial exactly when its algebra is split, which the four-fold splitting criterion translates into the solvability of the norm equation b = x² - ay² and into the isotropy of ⟨1, -a, -b⟩.

Main results

• TauCeti.BrauerGroup.quaternionCSA: the bundled central simple algebra of a quaternion symbol with unit parameters.
• TauCeti.BrauerGroup.quaternionClass: the Brauer class of that symbol.
• TauCeti.BrauerGroup.quaternionClass_eq_iff: two symbols have the same class exactly when their algebras are isomorphic, and TauCeti.BrauerGroup.quaternionClass_eq_one_iff: a symbol is trivial exactly when its algebra is split.
• TauCeti.BrauerGroup.quaternionClass_comm, TauCeti.BrauerGroup.quaternionClass_sq, TauCeti.BrauerGroup.quaternionClass_mul_sq_right, TauCeti.BrauerGroup.quaternionClass_one_sub: symmetry, 2-torsion, square-class invariance and the Steinberg relation.
• TauCeti.BrauerGroup.quaternionClass_mul, TauCeti.BrauerGroup.quaternionClass_mul_left: bilinearity of the quaternion symbol.
• TauCeti.BrauerGroup.quaternionClassOnSquareClasses: the symbol as a pairing of square classes, which is symmetric and bilinear (quaternionClassOnSquareClasses_comm, quaternionClassOnSquareClasses_add_left, quaternionClassOnSquareClasses_add_right).
• TauCeti.BrauerGroup.quaternionClass_congr: isometric binary forms ⟨a,b⟩ ≅ ⟨c,d⟩ have equal symbols [(a,b)] = [(c,d)].

References

The classical central-simple background is in T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter III, §2, in particular Theorem 2.11 for the symbol relations, and P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), §1.1 and Lemma 1.5.2.

noncomputable def TauCeti.BrauerGroup.quaternionCSA {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : CSA K

The bundled central simple algebra underlying the quaternion symbol (a,b).

Equations

• TauCeti.BrauerGroup.quaternionCSA a b = TauCeti.CSA.of K (QuaternionAlgebra K (↑a) 0 ↑b)

@[simp]

theorem TauCeti.BrauerGroup.quaternionCSA_def {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionCSA a b = CSA.of K (QuaternionAlgebra K (↑a) 0 ↑b)

The bundled algebra underlying quaternionCSA is the corresponding quaternion symbol.

noncomputable def TauCeti.BrauerGroup.quaternionClass {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : BrauerGroup K

The Brauer class of the quaternion symbol (a,b) for unit parameters a b : Kˣ.

Equations

• TauCeti.BrauerGroup.quaternionClass a b = TauCeti.BrauerGroup.mk (TauCeti.BrauerGroup.quaternionCSA a b)

theorem TauCeti.BrauerGroup.quaternionClass_def {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionClass a b = mk (CSA.of K (QuaternionAlgebra K (↑a) 0 ↑b))

The defining equation for quaternionClass. Not a simp lemma: the symbol is the normal form the relations below are stated in, and unfolding it to a bare Brauer class would defeat them.

Transporting along algebra isomorphisms

theorem TauCeti.BrauerGroup.quaternionClass_eq_of_algEquiv {K : Type u_1} [Field K] [Invertible 2] {a b c d : Kˣ} (e : QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] QuaternionAlgebra K (↑c) 0 ↑d) : quaternionClass a b = quaternionClass c d

An isomorphism of quaternion algebras identifies the two symbols.

theorem TauCeti.BrauerGroup.quaternionClass_eq_one_of_algEquiv_matrix {K : Type u_1} [Field K] [Invertible 2] {a b : Kˣ} (e : QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K) : quaternionClass a b = 1

A split quaternion symbol has trivial class.

theorem TauCeti.BrauerGroup.quaternionClass_eq_one_iff {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionClass a b = 1 ↔ Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)

A quaternion symbol is trivial in the Brauer group exactly when its algebra is split.

theorem TauCeti.BrauerGroup.quaternionClass_eq_one_iff_exists_eq_sq_sub_mul_sq {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionClass a b = 1 ↔ ∃ (x : K) (y : K), ↑b = x ^ 2 - ↑a * y ^ 2

A quaternion symbol is trivial exactly when the norm equation b = x² - ay² is solvable (the four-fold splitting criterion, read in the Brauer group).

theorem TauCeti.BrauerGroup.quaternionClass_eq_one_iff_not_anisotropic_weightedSumSquares {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionClass a b = 1 ↔ ¬(QuadraticMap.weightedSumSquares K ![1, -↑a, -↑b]).Anisotropic

A quaternion symbol is trivial exactly when ⟨1, -a, -b⟩ is isotropic (the four-fold splitting criterion, read in the Brauer group).

theorem TauCeti.BrauerGroup.quaternionClass_eq_iff {K : Type u_1} [Field K] [Invertible 2] (a b c d : Kˣ) : quaternionClass a b = quaternionClass c d ↔ Nonempty (QuaternionAlgebra K (↑a) 0 ↑b ≃ₐ[K] QuaternionAlgebra K (↑c) 0 ↑d)

Two quaternion symbols have the same Brauer class exactly when their algebras are isomorphic. Both algebras are division algebras or both are split, since the class detects splitting; in the division case this is the uniqueness of the division-algebra representative of a Brauer class.

Symmetry, square classes and two-torsion

theorem TauCeti.BrauerGroup.quaternionClass_comm {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionClass a b = quaternionClass b a

Symmetry of the quaternion symbol: [(a,b)] = [(b,a)].

theorem TauCeti.BrauerGroup.quaternionClass_mul_sq_right {K : Type u_1} [Field K] [Invertible 2] (a b c : Kˣ) : quaternionClass a (b * c ^ 2) = quaternionClass a b

The quaternion symbol is invariant under multiplying its second argument by a square.

theorem TauCeti.BrauerGroup.quaternionClass_mul_sq_left {K : Type u_1} [Field K] [Invertible 2] (a b c : Kˣ) : quaternionClass (a * c ^ 2) b = quaternionClass a b

The quaternion symbol is invariant under multiplying its first argument by a square.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_inv_right {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionClass a b⁻¹ = quaternionClass a b

Inverting the second argument does not change a quaternion symbol.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_inv_left {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionClass a⁻¹ b = quaternionClass a b

Inverting the first argument does not change a quaternion symbol.

@[simp]

theorem TauCeti.BrauerGroup.inv_quaternionClass {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : (quaternionClass a b)⁻¹ = quaternionClass a b

The quaternion symbol is its own inverse: quaternion conjugation is an isomorphism of ℍ[K,a,b] with its opposite algebra.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_sq {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionClass a b ^ 2 = 1

The quaternion symbol is 2-torsion: [(a,b)]² = 1.

The split symbols

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_one_left {K : Type u_1} [Field K] [Invertible 2] (b : Kˣ) : quaternionClass 1 b = 1

[(1,b)] = 1.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_one_right {K : Type u_1} [Field K] [Invertible 2] (a : Kˣ) : quaternionClass a 1 = 1

[(a,1)] = 1.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_neg_self {K : Type u_1} [Field K] [Invertible 2] (a : Kˣ) : quaternionClass a (-a) = 1

[(a,-a)] = 1.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_sq_right {K : Type u_1} [Field K] [Invertible 2] (a c : Kˣ) : quaternionClass a (c ^ 2) = 1

[(a,c²)] = 1: square-class invariance at [(a,1)] = 1.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_sq_left {K : Type u_1} [Field K] [Invertible 2] (b c : Kˣ) : quaternionClass (c ^ 2) b = 1

[(c²,b)] = 1: square-class invariance at [(1,b)] = 1.

theorem TauCeti.BrauerGroup.quaternionClass_one_sub {K : Type u_1} [Field K] [Invertible 2] (a : Kˣ) (h : 1 - ↑a ≠ 0) : quaternionClass a (Units.mk0 (1 - ↑a) h) = 1

The Steinberg relation [(a,1-a)] = 1, for a unit a with 1 - a ≠ 0.

Bilinearity

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_mul {K : Type u_1} [Field K] [Invertible 2] (a b c : Kˣ) : quaternionClass a (b * c) = quaternionClass a b * quaternionClass a c

Bilinearity of the quaternion symbol in the second argument: [(a,bc)] = [(a,b)] · [(a,c)]. This is the common slot lemma ℍ[K,a,b] ⊗[K] ℍ[K,a,c] ≃ₐ[K] ℍ[K,a,bc] ⊗[K] M₂(K) read in the Brauer group.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_mul_left {K : Type u_1} [Field K] [Invertible 2] (a b c : Kˣ) : quaternionClass (a * b) c = quaternionClass a c * quaternionClass b c

Bilinearity of the quaternion symbol in the first argument: [(ab,c)] = [(a,c)] · [(b,c)].

theorem TauCeti.BrauerGroup.quaternionClass_self {K : Type u_1} [Field K] [Invertible 2] (a : Kˣ) : quaternionClass a a = quaternionClass a (-1)

[(a,a)] = [(a,-1)], since a = (-1) · (-a) and [(a,-a)] = 1.

theorem TauCeti.BrauerGroup.quaternionClass_neg_inv_mul_neg_inv_mul {K : Type u_1} [Field K] [Invertible 2] (a b c : Kˣ) : quaternionClass (-c⁻¹ * a) (-c⁻¹ * b) = quaternionClass a b * quaternionClass a c * quaternionClass b c * quaternionClass (-1) (a * b * c) * quaternionClass (-1) (-1)

The symbol [(-a/c, -b/c)] expanded by bilinearity: [(a,b)] · [(a,c)] · [(b,c)] · [(-1,abc)] · [(-1,-1)]. This is the symbol identity behind the ternary case of Lam's Clifford--Hasse comparison.

The symbol on square classes

noncomputable def TauCeti.BrauerGroup.quaternionClassOnSquareClasses {K : Type u_1} [Field K] [Invertible 2] (x y : SquareClassGroup K) : BrauerGroup K

The quaternion symbol factored through the square classes of its two parameters.

Equations

• TauCeti.BrauerGroup.quaternionClassOnSquareClasses x y = TauCeti.BrauerGroup.quaternionClass (Additive.toMul (Quotient.out x)) (Additive.toMul (Quotient.out y))

@[simp]

theorem TauCeti.BrauerGroup.quaternionClassOnSquareClasses_squareClass {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : quaternionClassOnSquareClasses (squareClass a) (squareClass b) = quaternionClass a b

The square-class pairing agrees with the quaternion symbol on representatives.

theorem TauCeti.BrauerGroup.quaternionClassOnSquareClasses_comm {K : Type u_1} [Field K] [Invertible 2] (x y : SquareClassGroup K) : quaternionClassOnSquareClasses x y = quaternionClassOnSquareClasses y x

The square-class pairing is symmetric.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClassOnSquareClasses_add_left {K : Type u_1} [Field K] [Invertible 2] (x y z : SquareClassGroup K) : quaternionClassOnSquareClasses (x + y) z = quaternionClassOnSquareClasses x z * quaternionClassOnSquareClasses y z

The square-class pairing is additive in its first argument.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClassOnSquareClasses_add_right {K : Type u_1} [Field K] [Invertible 2] (x y z : SquareClassGroup K) : quaternionClassOnSquareClasses x (y + z) = quaternionClassOnSquareClasses x y * quaternionClassOnSquareClasses x z

The square-class pairing is additive in its second argument.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClassOnSquareClasses_zero_left {K : Type u_1} [Field K] [Invertible 2] (y : SquareClassGroup K) : quaternionClassOnSquareClasses 0 y = 1

The square-class pairing is trivial when its first argument is the trivial class.

@[simp]

theorem TauCeti.BrauerGroup.quaternionClassOnSquareClasses_zero_right {K : Type u_1} [Field K] [Invertible 2] (x : SquareClassGroup K) : quaternionClassOnSquareClasses x 0 = 1

The square-class pairing is trivial when its second argument is the trivial class.

Invariance under isometry of binary forms

theorem TauCeti.BrauerGroup.quaternionClass_congr {K : Type u_1} [Field K] [Invertible 2] {a b c d : Kˣ} (h : (QuadraticMap.weightedSumSquares K ![↑a, ↑b]).Equivalent (QuadraticMap.weightedSumSquares K ![↑c, ↑d])) : quaternionClass a b = quaternionClass c d

The quaternion symbol is an invariant of the binary form ⟨a,b⟩: isometric binary forms have equal symbols. This is the binary quaternion lemma read in the Brauer group, and it is what makes the Hasse invariant well defined on isometry classes.