The value of the Evens norm on a Kummer class

Let L = K(x) be a separable quadratic extension of a field K in which 2 is invertible, with x² = d ∈ Kˣ, and let σ : L → Kˢ be a K-embedding. For a ∈ Lˣ, the Evens norm N^{Ev}((a)) ∈ H²(G_K, 𝔽₂) of the Kummer class (a) ∈ H¹(G_L, 𝔽₂) is (Kahn, Lemme II.2.1)

N^{Ev}((a)) = (Tr a) ∪ (−d · N a) + (2) ∪ (d)       if Tr a ≠ 0,
N^{Ev}((a)) = (2) ∪ (d)                             if Tr a = 0

(TauCeti.galoisEvens2_kummerClass, TauCeti.galoisEvens2_kummerClass_of_trace_eq_zero). Both are specializations of Serre's formula N^{Ev}((a)) = (w₁) ∪ (w₀) + (2) ∪ (d) for the values w₀, w₁ of any orthogonal basis of the twisted trace form Tr_*⟨a⟩ : y ↦ Tr (a y²) (TauCeti.galoisEvens2_kummerClass_eq_cup_add_cup), that is w₂(Tr_*⟨a⟩) = N^{Ev}((a)) + (2) ∪ (d).

The results hold for K and L in any universe.

Main results

• TauCeti.galoisEvens2_kummerClass_eq_cup_add_cup: N^{Ev}((a)) = (w₁) ∪ (w₀) + (2) ∪ (d) for the values w₀, w₁ of any orthogonal basis of Tr_*⟨a⟩.
• TauCeti.galoisEvens2_kummerClass: N^{Ev}((a)) = (Tr a) ∪ (−d · N a) + (2) ∪ (d) if Tr a ≠ 0.
• TauCeti.galoisEvens2_kummerClass_of_trace_eq_zero: N^{Ev}((a)) = (2) ∪ (d) if Tr a = 0.
• TauCeti.galoisEvens2_kummerClass_algebraMap_mul: for c ∈ Kˣ, N^{Ev}((c a)) = N^{Ev}((a)) + (c) ∪ (−d · N a).
• TauCeti.galoisEvens2_kummerClass_one_add: N^{Ev}((1 + t x)) = (2) ∪ (1 − t² d).
• TauCeti.galoisEvens2_kummerClass_sqrt: N^{Ev}((x)) = (2) ∪ (d).

References

• B. Kahn, Classes de Stiefel-Whitney de formes quadratiques et de représentations galoisiennes réelles, Invent. Math. 78 (1984), 223–256, Lemme II.2.1.
• J.-P. Serre, L'invariant de Witt de la forme Tr(x²), Comment. Math. Helv. 59 (1984), 651–676, Théorème 1′ and its second proof.

theorem TauCeti.galoisEvens2_kummerClass_eq_cup_add_cup {K : Type u} [Field K] [Invertible 2] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (d : Kˣ) {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) ↑d) (a : Lˣ) (y : Fin 2 → L) (hy : (Algebra.trace K L) (↑a * y 0 * y 1) = 0) (w : Fin 2 → Kˣ) (hw : ∀ (i : Fin 2), ↑(w i) = (Algebra.trace K L) (↑a * y i ^ 2)) : galoisEvens K L σ hdeg (kummerClass a) = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass (w 1))) (kummerClass (w 0)) + (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass (unitOfInvertible 2))) (kummerClass d)

Serre's formula for the Evens norm of a Kummer class (Serre, Théorème 1′ at n = 2): for an orthogonal basis y of the twisted trace form Tr_*⟨a⟩ : z ↦ Tr (a z²) whose values w_j = Tr (a y_j²) are units,

N^{Ev}((a)) = (w₁) ∪ (w₀) + (2) ∪ (d),

where d is the square of a generator x of L = K(x). Since (w₀) ∪ (w₁) is the second Stiefel–Whitney class of ⟨w₀, w₁⟩ ≅ Tr_*⟨a⟩, this is w₂(Tr_*⟨a⟩) = N^{Ev}((a)) + (2) ∪ (d).

theorem TauCeti.galoisEvens2_kummerClass_of_trace_eq_zero {K : Type u} [Field K] [Invertible 2] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (d : Kˣ) {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) ↑d) (a : Lˣ) (ht : (Algebra.trace K L) ↑a = 0) : galoisEvens K L σ hdeg (kummerClass a) = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass (unitOfInvertible 2))) (kummerClass d)

The value of the Evens norm on a Kummer class at trace zero (Kahn, Lemme II.2.1): if Tr a = 0, then N^{Ev}((a)) = (2) ∪ (d).

theorem TauCeti.galoisEvens2_kummerClass_sqrt {K : Type u} [Field K] [Invertible 2] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (d : Kˣ) {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) ↑d) (b : Lˣ) (hb : ↑b = x) : galoisEvens K L σ hdeg (kummerClass b) = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass (unitOfInvertible 2))) (kummerClass d)

The Evens norm of the square root x of d: N^{Ev}((x)) = (2) ∪ (d), the trace-zero case of TauCeti.galoisEvens2_kummerClass_of_trace_eq_zero at a = x.

theorem TauCeti.galoisEvens2_kummerClass {K : Type u} [Field K] [Invertible 2] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (d : Kˣ) {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) ↑d) (a : Lˣ) (t : Kˣ) (ht : ↑t = (Algebra.trace K L) ↑a) : galoisEvens K L σ hdeg (kummerClass a) = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass t)) (kummerClass (-(d * (Units.map (Algebra.norm K)) a))) + (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass (unitOfInvertible 2))) (kummerClass d)

The value of the Evens norm on a Kummer class (Kahn, Lemme II.2.1): if Tr a = t ≠ 0, then

N^{Ev}((a)) = (Tr a) ∪ (−d · N a) + (2) ∪ (d).

theorem TauCeti.galoisEvens2_kummerClass_algebraMap_mul {K : Type u} [Field K] [Invertible 2] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (d : Kˣ) {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) ↑d) (c : Kˣ) (a : Lˣ) : galoisEvens K L σ hdeg (kummerClass ((Units.map ↑(algebraMap K L)) c * a)) = galoisEvens K L σ hdeg (kummerClass a) + (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass c)) (kummerClass (-(d * (Units.map (Algebra.norm K)) a)))

The Evens norm of a Kummer class scaled by a base unit: for c ∈ Kˣ and a ∈ Lˣ,

N^{Ev}((c a)) = N^{Ev}((a)) + (c) ∪ (−d · N a).

If Tr a = 0, then −d · N a is a square and the correction term vanishes.

The norm of 1 + t √d

theorem TauCeti.galoisEvens2_kummerClass_one_add {K : Type u} [Field K] [Invertible 2] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (d : Kˣ) {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) ↑d) (t : K) (ht : 1 - t ^ 2 * ↑d ≠ 0) (b : Lˣ) (hb : ↑b = 1 + (algebraMap K L) t * x) : galoisEvens K L σ hdeg (kummerClass b) = (((trivialF2TopPairing (AbsoluteGaloisGroup K)).cup 1 1) (kummerClass (unitOfInvertible 2))) (kummerClass (Units.mk0 (1 - t ^ 2 * ↑d) ht))

The Evens norm of 1 + t √d: N^{Ev}((1 + t x)) = (2) ∪ (1 − t² d).