Comparing the two Hasse invariants over a local field

Applying the canonical sign isomorphism on the quaternion subgroup of the Brauer group to the Brauer-valued Hasse invariant gives the local Hasse invariant, since both invariants are products over pairs of diagonal coefficients. This comparison uses the local classification of quaternion algebras and requires no cohomological invariant map.

Main results

• TauCeti.RegularFormClass.quaternionSubgroupSignEquiv_apply_hasseInvariant: the comparison of Brauer-valued and sign-valued Hasse invariants.
• TauCeti.RegularFormClass.localHasse_mk_neg_neg_mul: the Hasse sign of a pure quaternion norm form, obtained from its Brauer-valued invariant.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapters V, §3 and VI, §2.
• J.-P. Serre, A Course in Arithmetic, Chapter IV, §2.

@[simp]

theorem TauCeti.RegularFormClass.quaternionSubgroupSignEquiv_apply_hasseInvariant {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (q : RegularFormClass K) : BrauerGroup.quaternionSubgroupSignEquiv ⟨q.hasseInvariant, ⋯⟩ = q.localHasse

The two Hasse invariants agree. The sign isomorphism on the quaternion subgroup carries the Brauer-valued Hasse invariant to the local Hasse invariant.

@[simp]

theorem TauCeti.RegularFormClass.localHasse_mk_neg_neg_mul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] (a b : Kˣ) : localHasse ⟦⟨3, ![-a, -b, a * b]⟩⟧ = hilbertSymbol a b * hilbertSymbol (-1) (-1)

The Hasse sign of the pure quaternion norm form ⟨-a, -b, ab⟩ is (a,b) · (-1,-1). This takes priority over the general diagonal product formula.