The subgroup generated by quaternion classes

The quaternion subgroup of the Brauer group is generated by the classes of the quaternion algebras ℍ[K,a,b], for units a and b. Products of quaternion classes, such as the Hasse invariant of a regular quadratic form, belong to this subgroup. Over a general field a product need not itself be the class of a quaternion algebra.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter V, §3.

def TauCeti.BrauerGroup.quaternionSubgroup (K : Type u_1) [Field K] [Invertible 2] : Subgroup (BrauerGroup K)

The subgroup of the Brauer group generated by quaternion algebra classes.

Equations

• TauCeti.BrauerGroup.quaternionSubgroup K = Subgroup.closure (Set.range fun (ab : Kˣ × Kˣ) => TauCeti.BrauerGroup.quaternionClass ab.1 ab.2)

@[simp]

theorem TauCeti.BrauerGroup.quaternionClass_mem_quaternionSubgroup (K : Type u_1) [Field K] [Invertible 2] (a b : Kˣ) : quaternionClass a b ∈ quaternionSubgroup K

Every quaternion symbol belongs to the quaternion subgroup.