The Hasse invariant of a regular quadratic form

Over a field K in which two is invertible, a regular quadratic form q is diagonalizable, q ≅ ⟨a₁, …, aₙ⟩, and its Hasse invariant is the product of quaternion symbols s(q) = ∏_{i<j} [(aᵢ, aⱼ)] in the Brauer group of K, with the empty product in ranks 0 and 1. This is the convention of Lam (V.3.17) and of Serre's ε (A Course in Arithmetic, IV.2.1); O'Meara's Hasse symbol ∏_{i≤j} (aᵢ, aⱼ) differs from it by a correction term.

The invariant is defined on TauCeti.RegularFormClass, so it depends only on the isometry class of the form. That the product does not depend on the chosen diagonalization is Witt's chain theorem, through the descent principle TauCeti.RegularFormClass.liftDiagonal: the product is unchanged by permuting the coefficients because the symbol is symmetric, and by replacing two coefficients with those of an isometric binary form because the symbol is bilinear and takes equal values on isometric binary forms (Lam V.3.18).

Every symbol is 2-torsion, so the Hasse invariant takes values in the 2-torsion of the Brauer group. It is a genuine invariant beyond rank and discriminant: over ℝ the forms ⟨1, 1⟩ and ⟨-1, -1⟩ have the same rank and the same discriminant, and different Hasse invariants.

Main definitions

• TauCeti.RegularFormClass.hasseInvariant: the Hasse invariant of an isometry class of regular quadratic forms.

Main results

• TauCeti.RegularFormClass.hasseInvariant_mk: its value ∏_{i<j} [(aᵢ, aⱼ)] on a diagonal presentation ⟨a₁, …, aₙ⟩.
• TauCeti.RegularFormClass.omearaHasseSymbol_eq: O'Meara's i ≤ j symbol is the Lam–Serre Hasse invariant times the symbol of the discriminant with -1.
• TauCeti.RegularFormClass.hasseInvariant_formClass: the same value on the class of any regular form isometric to ⟨a₁, …, aₙ⟩.
• TauCeti.RegularFormClass.hasseInvariant_eq_one_of_rank_le_one: the invariant is trivial in ranks 0 and 1, in particular on 0, on 1 and on every ⟨a⟩.
• TauCeti.RegularFormClass.hasseInvariant_mk_binary: s⟨a, b⟩ = [(a, b)].
• TauCeti.RegularFormClass.hasseInvariant_add_mk: the orthogonal-sum formula on diagonal presentations.
• TauCeti.RegularFormClass.hasseInvariant_add: the formula for arbitrary classes, with its cross term expressed through their discriminants.
• TauCeti.RegularFormClass.hasseInvariant_mk_scale: the formula for scaling a diagonal presentation by a unit.
• TauCeti.RegularFormClass.hasseInvariant_mk_rankOne_mul_mk: the same scaling formula for multiplication by the rank-one class.
• TauCeti.RegularFormClass.hasseInvariant_mk_rankOne_mul: the scaling formula for any class.
• TauCeti.RegularFormClass.hasseInvariant_mk_neg_neg_mul: the Hasse invariant of the pure quaternion norm form ⟨-a, -b, ab⟩.
• TauCeti.RegularFormClass.hasseInvariant_hyperbolicClass: the hyperbolic plane has trivial Hasse invariant.
• TauCeti.RegularFormClass.hasseInvariant_sq: the invariant is 2-torsion.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Graduate Studies in Mathematics 67, American Mathematical Society (2005), Chapter V, Definition 3.17 and Proposition 3.18.
• J.-P. Serre, A Course in Arithmetic, Graduate Texts in Mathematics 7, Springer (1973), Chapter IV, §2.1.
• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), §63:20.

noncomputable def TauCeti.RegularFormClass.hasseInvariant {K : Type u} [Field K] [Invertible 2] : RegularFormClass K → BrauerGroup K

The Hasse invariant of an isometry class of regular quadratic forms: for a diagonal presentation ⟨a₁, …, aₙ⟩ of the class, the product ∏_{i<j} [(aᵢ, aⱼ)] of quaternion symbols in the Brauer group, which is 1 in ranks 0 and 1. It does not depend on the presentation.

@[simp]

theorem TauCeti.RegularFormClass.hasseInvariant_mk {K : Type u} [Field K] [Invertible 2] (p : RegularFormPresentation K) : hasseInvariant ⟦p⟧ = ∏ i : Fin p.fst, ∏ j > i, BrauerGroup.quaternionClass (p.snd i) (p.snd j)

The Hasse invariant of the class of a diagonal presentation ⟨a₁, …, aₙ⟩ is ∏_{i<j} [(aᵢ, aⱼ)].

@[simp]

theorem TauCeti.RegularFormClass.hasseInvariant_mem_quaternionSubgroup {K : Type u} [Field K] [Invertible 2] (q : RegularFormClass K) : q.hasseInvariant ∈ BrauerGroup.quaternionSubgroup K

The Hasse invariant belongs to the subgroup generated by quaternion classes.

theorem TauCeti.RegularFormClass.omearaHasseSymbol_eq {K : Type u} [Field K] [Invertible 2] (p : RegularFormPresentation K) : ∏ i : Fin p.fst, ∏ j ≥ i, BrauerGroup.quaternionClass (p.snd i) (p.snd j) = hasseInvariant ⟦p⟧ * BrauerGroup.quaternionClassOnSquareClasses (discr ⟦p⟧) (squareClass (-1))

O'Meara's Hasse symbol ∏_{i≤j} [(aᵢ,aⱼ)] equals the Lam–Serre Hasse invariant ∏_{i<j} [(aᵢ,aⱼ)] times [(d(q),-1)]. The diagonal correction uses [(a,a)] = [(a,-1)], so the discriminant here is the unsigned one.

theorem TauCeti.RegularFormClass.hasseInvariant_formClass {K : Type u} [Field K] [Invertible 2] {V : Type u_1} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {n : ℕ} (w : Fin n → Kˣ) (h : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(w i))) : (formClass Q hQ).hasseInvariant = ∏ i : Fin n, ∏ j > i, BrauerGroup.quaternionClass (w i) (w j)

The Hasse invariant of a regular form isometric to ⟨a₁, …, aₙ⟩ is ∏_{i<j} [(aᵢ, aⱼ)].

theorem TauCeti.RegularFormClass.hasseInvariant_eq_one_of_rank_le_one {K : Type u} [Field K] [Invertible 2] {x : RegularFormClass K} (hx : x.rank ≤ 1) : x.hasseInvariant = 1

The Hasse invariant is trivial in ranks 0 and 1.

@[simp]

theorem TauCeti.RegularFormClass.hasseInvariant_zero {K : Type u} [Field K] [Invertible 2] : hasseInvariant 0 = 1

The zero class has trivial Hasse invariant.

@[simp]

theorem TauCeti.RegularFormClass.hasseInvariant_one {K : Type u} [Field K] [Invertible 2] : hasseInvariant 1 = 1

The unit class ⟨1⟩ has trivial Hasse invariant.

theorem TauCeti.RegularFormClass.hasseInvariant_mk_rankOne {K : Type u} [Field K] [Invertible 2] (a : Kˣ) : hasseInvariant ⟦⟨1, fun (x : Fin 1) => a⟩⟧ = 1

A rank-one form ⟨a⟩ has trivial Hasse invariant.

@[simp]

theorem TauCeti.RegularFormClass.hasseInvariant_mk_binary {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : hasseInvariant ⟦⟨2, ![a, b]⟩⟧ = BrauerGroup.quaternionClass a b

The Hasse invariant of a binary form ⟨a, b⟩ is the quaternion symbol [(a, b)]. This takes priority over hasseInvariant_mk, whose product the simplifier does not evaluate on Fin 2.

theorem TauCeti.RegularFormClass.hasseInvariant_add_mk {K : Type u} [Field K] [Invertible 2] (p q : RegularFormPresentation K) : hasseInvariant (⟦p⟧ + ⟦q⟧) = hasseInvariant ⟦p⟧ * hasseInvariant ⟦q⟧ * BrauerGroup.quaternionClass (∏ i : Fin p.fst, p.snd i) (∏ j : Fin q.fst, q.snd j)

Orthogonal-sum formula on diagonal presentations: the cross term is the quaternion symbol of their coefficient products, which represent their discriminants.

theorem TauCeti.RegularFormClass.hasseInvariant_mk_scale {K : Type u} [Field K] [Invertible 2] (a : Kˣ) (p : RegularFormPresentation K) : hasseInvariant ⟦⟨p.fst, fun (i : Fin p.fst) => a * p.snd i⟩⟧ = hasseInvariant ⟦p⟧ * BrauerGroup.quaternionClass a (-1) ^ p.fst.choose 2 * BrauerGroup.quaternionClass a (∏ i : Fin p.fst, p.snd i) ^ (p.fst - 1)

Scaling formula on a diagonal presentation: the first correction counts coefficient pairs, and the second uses the product of coefficients representing the discriminant.

theorem TauCeti.RegularFormClass.hasseInvariant_mk_rankOne_mul_mk {K : Type u} [Field K] [Invertible 2] (a : Kˣ) (p : RegularFormPresentation K) : hasseInvariant (⟦⟨1, fun (x : Fin 1) => a⟩⟧ * ⟦p⟧) = hasseInvariant ⟦p⟧ * BrauerGroup.quaternionClass a (-1) ^ p.fst.choose 2 * BrauerGroup.quaternionClass a (∏ i : Fin p.fst, p.snd i) ^ (p.fst - 1)

Scaling by a rank-one class is coefficientwise scaling of a diagonal presentation. The Hasse-invariant correction is expressed through the presentation's rank and coefficient product.

theorem TauCeti.RegularFormClass.hasseInvariant_add {K : Type u} [Field K] [Invertible 2] (x y : RegularFormClass K) : (x + y).hasseInvariant = x.hasseInvariant * y.hasseInvariant * BrauerGroup.quaternionClassOnSquareClasses x.discr y.discr

Orthogonal-sum formula for regular-form classes: the cross term is the quaternion symbol of their discriminants.

theorem TauCeti.RegularFormClass.hasseInvariant_mk_rankOne_mul {K : Type u} [Field K] [Invertible 2] (a : Kˣ) (x : RegularFormClass K) : hasseInvariant (⟦⟨1, fun (x : Fin 1) => a⟩⟧ * x) = x.hasseInvariant * BrauerGroup.quaternionClass a (-1) ^ x.rank.choose 2 * BrauerGroup.quaternionClassOnSquareClasses (squareClass a) x.discr ^ (x.rank - 1)

Scaling formula for any regular-form class: multiplying by ⟨a⟩ changes the Hasse invariant by a rank-dependent sign symbol and a symbol with its discriminant.

@[simp]

theorem TauCeti.RegularFormClass.hasseInvariant_hyperbolicClass {K : Type u} [Field K] [Invertible 2] : (hyperbolicClass K).hasseInvariant = 1

The hyperbolic plane ⟨1, -1⟩ has trivial Hasse invariant.

@[simp]

theorem TauCeti.RegularFormClass.hasseInvariant_sq {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : x.hasseInvariant ^ 2 = 1

The Hasse invariant is 2-torsion: it lies in the 2-torsion of the Brauer group.

@[simp]

theorem TauCeti.RegularFormClass.hasseInvariant_mk_neg_neg_mul {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : hasseInvariant ⟦⟨3, ![-a, -b, a * b]⟩⟧ = BrauerGroup.quaternionClass a b * BrauerGroup.quaternionClass (-1) (-1)

The Hasse invariant of a pure quaternion norm form: the ternary form ⟨-a, -b, ab⟩, which is the norm form of ℍ[K,a,b] on its pure quaternions, has Hasse invariant [(a, b)] · [(-1, -1)].