Scalar extension of the Hasse invariant

The Brauer-valued Hasse invariant commutes with extension of scalars: the invariant of an extended quadratic space is the image of its original invariant under the scalar-extension homomorphism on Brauer groups. This permits the same invariant to be compared over different fields without choosing compatible diagonalizations.

The convention is Lam's s(q) = ∏_{i<j} [(aᵢ,aⱼ)], with the empty product in ranks zero and one. Scalar extension preserves each quaternion symbol by TauCeti.BrauerGroup.baseChange_quaternionClass, and hence preserves the product. No finiteness or separability assumption on the field extension is needed.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter V, §3, Definition 3.17 and Proposition 3.18.

@[simp]

theorem TauCeti.RegularFormClass.hasseInvariant_baseChange {K L : Type u} [Field K] [Field L] [Algebra K L] [Invertible 2] [Invertible 2] (q : RegularFormClass K) : (baseChange L q).hasseInvariant = (BrauerGroup.baseChange K L) q.hasseInvariant

The Hasse invariant of a scalar extension is the scalar extension of the original Brauer class.