The Stiefel–Whitney classes of an isometry class of regular forms

Let K be a field in which 2 is invertible. The Stiefel–Whitney classes w₁ = ∑ᵢ (aᵢ) and w₂ = ∑_{i<j} (aᵢ) ∪ (aⱼ) of a diagonal form ⟨a₁, …, aₙ⟩ (TauCeti.sw1, TauCeti.sw2) depend only on the isometry class of the form. In rank at least two, Witt's chain theorem reduces this to invariance under the two elementary steps of a diagonal chain; in rank one, where there is no binary step, it instead requires invariance when the single coefficient is multiplied by a square. The latter holds for w₁ because the Kummer class only depends on the square class, and for w₂ because it vanishes in rank one. Both classes are unchanged by permuting the coefficients. A binary step replaces two coefficients a, b by the coefficients c, d of an isometric binary form ⟨c, d⟩ ≅ ⟨a, b⟩; it leaves w₁ unchanged because the discriminants agree modulo squares, and it leaves w₂ unchanged because of the binary cup identity (a) ∪ (b) = (c) ∪ (d) (TauCeti.cup_kummerClass_congr): under the comparison of H²(G_K, 𝔽₂) with the Brauer group both sides are quaternion symbols, and isometric binary forms have equal quaternion symbols.

From these three invariance properties, the descent principle TauCeti.RegularFormClass.liftDiagonal produces functions TauCeti.sw1Class and TauCeti.sw2Class on TauCeti.RegularFormClass K, which agree with the tuple-level classes on every diagonal presentation. Composed with TauCeti.formClass, they are the Stiefel–Whitney classes w₁(q) and w₂(q) of a regular quadratic form q, and isometric regular forms have the same classes.

On these classes the two low-degree identities hold: w₁(q) = (d(q)) for the plain discriminant d, so w₁ is additive over orthogonal sums, and w₂(q ⊥ r) = w₂(q) + w₂(r) + w₁(q) ∪ w₁(r), the degree-two part of the product formula for Delzant's total class.

The binary cup identity rests on the comparison of the Brauer group with Galois cohomology. Both classes are defined for fields in any universe.

Main definitions

• TauCeti.sw1Class: the first Stiefel–Whitney class of an isometry class of regular forms.
• TauCeti.sw2Class: the second Stiefel–Whitney class of an isometry class of regular forms.
• TauCeti.sw1ClassHom: the first class as an additive homomorphism for the orthogonal sum.

Main results

• TauCeti.BinaryStep.sw2_eq: w₂ is invariant under a binary step of a diagonal chain.
• TauCeti.sw2_eq_of_equivalent: isometric diagonal forms have the same w₂.
• TauCeti.sw1Class_mk and TauCeti.sw2Class_mk: the classes of ⟨a₁, …, aₙ⟩ are computed on that presentation.
• TauCeti.sw1Class_formClass and TauCeti.sw2Class_formClass: the classes of a regular form are computed on any of its diagonalizations.
• TauCeti.sw1Class_eq_kummerSquareClassEquiv_discr: w₁(q) = (d(q)).
• TauCeti.sw1Class_add and TauCeti.sw2Class_add: w₁(q ⊥ r) = w₁(q) + w₁(r) and w₂(q ⊥ r) = w₂(q) + w₂(r) + w₁(q) ∪ w₁(r).
• TauCeti.sw1Class_mk_rankOne_mul: w₁(⟨c⟩ ⊗ q) = n · (c) + w₁(q) for q of rank n.
• TauCeti.sw1Class_formClass_congr and TauCeti.sw2Class_formClass_congr: isometric regular forms have the same classes.
• TauCeti.sw1Class_zero, TauCeti.sw2Class_zero, TauCeti.sw1Class_one, TauCeti.sw2Class_one, TauCeti.sw2Class_eq_zero_of_rank_le_one, TauCeti.sw1Class_mk_rankOne, TauCeti.sw2Class_mk_binary, TauCeti.sw1Class_hyperbolicClass and TauCeti.sw2Class_hyperbolicClass: the values in rank at most two, on the unit form and on the hyperbolic plane.

References

• J. Milnor, Algebraic K-theory and quadratic forms, Invent. Math. 9 (1970), §3.
• T. Y. Lam, Introduction to Quadratic Forms over Fields, Graduate Studies in Mathematics 67, American Mathematical Society (2005), Chapter I, Theorem 5.2, and Chapter V, Proposition 3.18.

The first class

noncomputable def TauCeti.sw1Class {K : Type u} [Field K] [Invertible 2] : RegularFormClass K → ↑(continuousCohomology 1 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat

The first Stiefel–Whitney class of an isometry class of regular forms: for a diagonal presentation ⟨a₁, …, aₙ⟩ of the class, the sum w₁ = ∑ᵢ (aᵢ) of the Kummer classes of its coefficients. It does not depend on the presentation.

@[simp]

theorem TauCeti.sw1Class_mk {K : Type u} [Field K] [Invertible 2] (p : RegularFormPresentation K) : sw1Class ⟦p⟧ = sw1 p.snd

w₁ of the class of a diagonal presentation ⟨a₁, …, aₙ⟩ is ∑ᵢ (aᵢ).

theorem TauCeti.sw1Class_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))) : sw1Class (formClass Q hQ) = sw1 w

w₁ of a regular form isometric to ⟨a₁, …, aₙ⟩ is ∑ᵢ (aᵢ).

theorem TauCeti.sw1Class_formClass_congr {K : Type u} [Field K] [Invertible 2] {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) {R : QuadraticForm K W} (hR : QuadraticMap.Nondegenerate) (h : QuadraticMap.Equivalent Q R) : sw1Class (formClass Q hQ) = sw1Class (formClass R hR)

w₁ is an isometry invariant of regular forms: isometric regular forms have the same first Stiefel–Whitney class.

@[simp]

theorem TauCeti.sw1Class_zero {K : Type u} [Field K] [Invertible 2] : sw1Class 0 = 0

The zero class has trivial w₁.

theorem TauCeti.sw1Class_eq_kummerSquareClassEquiv_discr {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : sw1Class x = (kummerSquareClassEquiv K) x.discr

w₁ is the Kummer class of the discriminant: w₁(q) = (d(q)), with the plain discriminant d and not the signed discriminant.

@[simp]

theorem TauCeti.sw1Class_add {K : Type u} [Field K] [Invertible 2] (x y : RegularFormClass K) : sw1Class (x + y) = sw1Class x + sw1Class y

w₁ is additive over orthogonal sums: w₁(q ⊥ r) = w₁(q) + w₁(r).

noncomputable def TauCeti.sw1ClassHom {K : Type u} [Field K] [Invertible 2] : RegularFormClass K →+ ↑(continuousCohomology 1 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat

w₁ as an additive homomorphism for the orthogonal sum.

@[simp]

theorem TauCeti.sw1ClassHom_apply {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : sw1ClassHom x = sw1Class x

The additive homomorphism TauCeti.sw1ClassHom is TauCeti.sw1Class.

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

w₁⟨a⟩ = (a).

theorem TauCeti.sw1Class_mk_rankOne_mul {K : Type u} [Field K] [Invertible 2] (c : Kˣ) (x : RegularFormClass K) : sw1Class (⟦⟨1, fun (x : Fin 1) => c⟩⟧ * x) = x.rank • kummerClass c + sw1Class x

Scaling formula for w₁: w₁(⟨c⟩ ⊗ q) = n · (c) + w₁(q) for q of rank n.

@[simp]

theorem TauCeti.sw1Class_one {K : Type u} [Field K] [Invertible 2] : sw1Class 1 = 0

The unit class ⟨1⟩ has trivial w₁.

@[simp]

theorem TauCeti.sw1Class_hyperbolicClass {K : Type u} [Field K] [Invertible 2] : sw1Class (hyperbolicClass K) = kummerClass (-1)

w₁ of the hyperbolic plane ⟨1, -1⟩ is (-1).

The second class

theorem TauCeti.BinaryStep.sw2_eq {K : Type u} [Field K] [Invertible 2] {n : ℕ} {w w' : Fin n → Kˣ} (h : BinaryStep w w') : sw2 w = sw2 w'

A binary step of a diagonal chain does not change w₂: replacing two coefficients of a diagonal form by the coefficients of an isometric binary form leaves ∑_{i<j} (aᵢ) ∪ (aⱼ) unchanged.

noncomputable def TauCeti.sw2Class {K : Type u} [Field K] [Invertible 2] : RegularFormClass K → ↑(continuousCohomology 2 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat

The second Stiefel–Whitney class of an isometry class of regular forms: for a diagonal presentation ⟨a₁, …, aₙ⟩ of the class, the sum w₂ = ∑_{i<j} (aᵢ) ∪ (aⱼ) of the cup products of the Kummer classes of pairs of distinct coefficients. It does not depend on the presentation.

@[simp]

theorem TauCeti.sw2Class_mk {K : Type u} [Field K] [Invertible 2] (p : RegularFormPresentation K) : sw2Class ⟦p⟧ = sw2 p.snd

w₂ of the class of a diagonal presentation ⟨a₁, …, aₙ⟩ is ∑_{i<j} (aᵢ) ∪ (aⱼ).

theorem TauCeti.sw2_eq_of_equivalent {K : Type u} [Field K] [Invertible 2] {p q : RegularFormPresentation K} (h : QuadraticMap.Equivalent (presentedForm p) (presentedForm q)) : sw2 p.snd = sw2 q.snd

w₂ is an isometry invariant of diagonal forms: isometric diagonal forms ⟨a₁, …, aₙ⟩ ≅ ⟨b₁, …, bₙ⟩ have the same second Stiefel–Whitney class.

theorem TauCeti.sw2Class_formClass {K : Type u} [Field K] [Invertible 2] {n : ℕ} {V : Type u_1} [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (w : Fin n → Kˣ) (h : QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(w i))) : sw2Class (formClass Q hQ) = sw2 w

w₂ of a regular form isometric to ⟨a₁, …, aₙ⟩ is ∑_{i<j} (aᵢ) ∪ (aⱼ).

theorem TauCeti.sw2Class_formClass_congr {K : Type u} [Field K] [Invertible 2] {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) {R : QuadraticForm K W} (hR : QuadraticMap.Nondegenerate) (h : QuadraticMap.Equivalent Q R) : sw2Class (formClass Q hQ) = sw2Class (formClass R hR)

w₂ is an isometry invariant of regular forms: isometric regular forms have the same second Stiefel–Whitney class.

@[simp]

theorem TauCeti.sw2Class_add {K : Type u} [Field K] [Invertible 2] (x y : RegularFormClass K) : sw2Class (x + y) = sw2Class x + sw2Class y + (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (sw1Class x)) (sw1Class y)

The orthogonal-sum formula for w₂: w₂(q ⊥ r) = w₂(q) + w₂(r) + w₁(q) ∪ w₁(r). The second Stiefel–Whitney class is not additive, and the defect is the cup product of the first classes.

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

w₂ vanishes in ranks 0 and 1, in particular on 0, on 1 and on every ⟨a⟩.

@[simp]

theorem TauCeti.sw2Class_zero {K : Type u} [Field K] [Invertible 2] : sw2Class 0 = 0

The zero class has trivial w₂.

@[simp]

theorem TauCeti.sw2Class_one {K : Type u} [Field K] [Invertible 2] : sw2Class 1 = 0

The unit class ⟨1⟩ has trivial w₂.

theorem TauCeti.sw2Class_mk_binary {K : Type u} [Field K] [Invertible 2] (a b : Kˣ) : sw2Class ⟦⟨2, ![a, b]⟩⟧ = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass a)) (kummerClass b)

w₂⟨a, b⟩ = (a) ∪ (b).

@[simp]

theorem TauCeti.sw2Class_hyperbolicClass {K : Type u} [Field K] [Invertible 2] : sw2Class (hyperbolicClass K) = 0

The hyperbolic plane ⟨1, -1⟩ has trivial w₂.