Central simple quaternion symbol algebras

This file proves centrality and simplicity for the general quaternion algebra ℍ[K,a,b,c]. For a field K with 2 invertible, simplicity holds when c * QuadraticAlgebra.discr a b ≠ 0: completing the square reduces this case to a symbol with both parameters units, for which the norm criterion gives either a division algebra or a two-by-two matrix algebra. The two-parameter symbol ℍ[K,a,b] is the specialization used by the Brauer-valued invariants.

Centrality only requires two to be regular: commuting with i and j forces the imaginary coordinates to vanish when either the j-square or the discriminant is regular. In particular, this applies over integral domains of characteristic different from two.

Main results

• TauCeti.QuaternionAlgebra.isSimpleRing_of_j_sq_mul_discr_ne_zero: a quaternion algebra with nonzero j-square and nonzero discriminant is simple.
• TauCeti.QuaternionAlgebra.instIsSimpleRing: quaternion symbol algebras with both parameters units are simple.
• TauCeti.QuaternionAlgebra.mem_center_iff and TauCeti.QuaternionAlgebra.isCentral_of_isLeftRegular_j_sq_or_isLeftRegular_discr: centrality when two is regular and either the j-square or the discriminant is regular.
• TauCeti.QuaternionAlgebra.isCentral_of_j_sq_ne_zero_or_discr_ne_zero: centrality over a domain of characteristic different from two, without requiring two to be invertible.
• TauCeti.QuaternionAlgebra.center_units_eq_range_unitsMap_algebraMap: the center of a quaternion unit group with unit symbols consists exactly of scalar units, over a base ring in which two is left-regular, including the split case.

The split/division dichotomy used here is the norm-equation criterion in TauCeti.Algebra.Quaternion.SplittingCriterion.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter III, §2.
• P. Gille and T. Szamuely, Central Simple Algebras and Galois Cohomology (2006), §1.1.

instance TauCeti.QuaternionAlgebra.instIsSimpleRing {K : Type u_1} [Field K] [Invertible 2] (a b : Kˣ) : IsSimpleRing (QuaternionAlgebra K (↑a) 0 ↑b)

A quaternion symbol with both parameters units is a simple ring.

theorem TauCeti.QuaternionAlgebra.isSimpleRing_of_j_sq_mul_discr_ne_zero {K : Type u_1} [Field K] [Invertible 2] {a b c : K} (h : c * QuadraticAlgebra.discr a b ≠ 0) : IsSimpleRing (QuaternionAlgebra K a b c)

A quaternion algebra with nonzero j-square and nonzero discriminant is simple.

@[simp]

theorem TauCeti.QuaternionAlgebra.mem_center_iff {K : Type u_1} [CommRing K] (a b c : K) (h2 : IsRegular 2) (h : IsRegular c ∨ IsRegular (QuadraticAlgebra.discr a b)) {x : QuaternionAlgebra K a b c} : x ∈ Subalgebra.center K (QuaternionAlgebra K a b c) ↔ x.imI = 0 ∧ x.imJ = 0 ∧ x.imK = 0

When two is regular and either the j-square or the discriminant is regular, an element of ℍ[K,a,b,c] is central iff its three imaginary coordinates vanish.

theorem TauCeti.QuaternionAlgebra.isCentral_of_isLeftRegular_j_sq_or_isLeftRegular_discr {K : Type u_1} [CommRing K] {a b c : K} (h2 : IsLeftRegular 2) (h : IsLeftRegular c ∨ IsLeftRegular (QuadraticAlgebra.discr a b)) : Algebra.IsCentral K (QuaternionAlgebra K a b c)

A quaternion algebra with left-regular j-square or left-regular discriminant is central when two is left-regular.

instance TauCeti.QuaternionAlgebra.instIsCentral {K : Type u_1} [CommRing K] (a : K) (b : Kˣ) [Invertible 2] : Algebra.IsCentral K (QuaternionAlgebra K a 0 ↑b)

A quaternion symbol whose second parameter b is a unit is central over its base ring.

theorem TauCeti.QuaternionAlgebra.center_units_eq_range_unitsMap_algebraMap {K : Type u_1} [CommRing K] (a b : Kˣ) (h2 : IsLeftRegular 2) : Subgroup.center (QuaternionAlgebra K (↑a) 0 ↑b)ˣ = (Units.map ↑(algebraMap K (QuaternionAlgebra K (↑a) 0 ↑b))).range

Over a base ring in which two is left-regular, the center of the unit group of a quaternion symbol with unit parameters is exactly the scalar units. This includes split quaternion algebras.

theorem TauCeti.QuaternionAlgebra.isCentral_of_j_sq_ne_zero_or_discr_ne_zero {K : Type u_1} [CommRing K] [NoZeroDivisors K] [NeZero 2] {a b c : K} (h : c ≠ 0 ∨ QuadraticAlgebra.discr a b ≠ 0) : Algebra.IsCentral K (QuaternionAlgebra K a b c)

Over a domain of characteristic different from two, a quaternion algebra with nonzero j-square or discriminant is central, even when two is not invertible.