The Evens norm of a mod-two Kummer class as a pullback of the D₁₆ class

Let L/K be a quadratic extension, σ : L →ₐ[K] Kˢ a K-embedding, and write G_L = galoisSubgroup K L σ, an open subgroup of index two in G_K. For a ∈ Lˣ choose a square root r ∈ Kˢ of σ a and an element s ∈ G_K ∖ G_L. The Kummer class (a) ∈ H¹(G_L, 𝔽₂) is the class of the Kummer character α_a : γ ↦ rootSign r γ of G_L (TauCeti.galoisF2Iso_inv_kummerClass), and its induced homomorphism

ρ_a = Ind α_a : G_K → C₂ ≀ C₂

at s is TauCeti.kummerInd. Read through the signed-permutation representation of C₂ ≀ C₂, ρ_a is the action of G_K on the roots r, s r of X² − σ a and X² − s (σ a); that reading is not formalised here.

Since the index-two Evens norm of the class of a continuous homomorphism is the pullback of the D₁₆ extension class c_{D₁₆} along its induced homomorphism (TauCeti.ContCohomology.evensNormIndexTwo_eq_ind_pullback), the Evens norm of the Kummer class is the class of the explicit 2-cocycle c_{D₁₆} ∘ (ρ_a × ρ_a) of G_K:

N^{Ev}((a)) = ρ_a^* c_{D₁₆}

(TauCeti.galoisEvens2_kummerClass_eq_pullback). This is the first step of Serre's computation of N^{Ev}((a)) in terms of Kummer classes of K, which evaluates c_{D₁₆} ∘ (ρ_a × ρ_a) through a lift of ρ_a to the dihedral group of order sixteen in Pin⁺₂.

Main definitions

• TauCeti.kummerInd: the induced homomorphism ρ_a = Ind α_a : G_K → C₂ ≀ C₂ of the Kummer character of a ∈ Lˣ on G_L.

Main results

• TauCeti.coordC_kummerInd: the swap coordinate of ρ_a(h) is rootSign (σ x) h for any x ∈ L ∖ K, the character of G_K with kernel G_L.
• TauCeti.galoisEvens2_kummerClass_eq_pullback: N^{Ev}((a)) is the class of c_{D₁₆} ∘ (ρ_a × ρ_a).

References

• J.-P. Serre, L'invariant de Witt de la forme Tr(x²), Comment. Math. Helv. 59 (1984), 651–676, §2.
• 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.

noncomputable def TauCeti.kummerInd {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) (s : AbsoluteGaloisGroup K) (hs : s ∉ galoisSubgroup K L σ) : AbsoluteGaloisGroup K →* WreathC2

The representation ρ_a = Ind α_a : G_K → C₂ ≀ C₂ of a ∈ Lˣ for a quadratic extension L/K: the induced homomorphism indexTwoInd, at an element s ∉ G_L, of the Kummer character α_a = galoisKummerCharacter σ a r hr of G_L = galoisSubgroup K L σ, for a square root r of σ a. Read through the signed-permutation representation of C₂ ≀ C₂, it is the action of G_K on the roots r, s r of X² − σ a and X² − s (σ a).

theorem TauCeti.kummerInd_def {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) (s : AbsoluteGaloisGroup K) (hs : s ∉ galoisSubgroup K L σ) : kummerInd σ hdeg a r hr s hs = ContCohomology.indexTwoInd ↑(galoisSubgroup K L σ) ⋯ s hs (galoisKummerCharacter σ a r hr)

kummerInd is the induced homomorphism of the Kummer character on galoisSubgroup K L σ.

theorem TauCeti.coordC_kummerInd {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) (s : AbsoluteGaloisGroup K) (hs : s ∉ galoisSubgroup K L σ) {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (h : AbsoluteGaloisGroup K) : ((kummerInd σ hdeg a r hr s hs) h).coordC = rootSign (σ x) h

The top coordinate of ρ_a(h) is rootSign (σ x) h for a generator x of the quadratic extension L = K(x): both are the character of G_K with kernel G_L.

theorem TauCeti.continuous_wreathD16Cocycle_kummerInd {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) (s : AbsoluteGaloisGroup K) (hs : s ∉ galoisSubgroup K L σ) : Continuous fun (q : AbsoluteGaloisGroup K × AbsoluteGaloisGroup K) => wreathD16Cocycle ((kummerInd σ hdeg a r hr s hs) q.1, (kummerInd σ hdeg a r hr s hs) q.2)

The pullback c_{D₁₆} ∘ (ρ_a × ρ_a) of the D₁₆ extension cocycle along kummerInd is continuous: ρ_a is locally constant, because galoisSubgroup K L σ is open and the Kummer character is continuous.

theorem TauCeti.galoisEvens2_kummerClass_eq_pullback {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) (s : AbsoluteGaloisGroup K) (hs : s ∉ galoisSubgroup K L σ) : galoisEvens K L σ hdeg (kummerClass a) = ContCohomology.f2CocycleClass (fun (q : AbsoluteGaloisGroup K × AbsoluteGaloisGroup K) => wreathD16Cocycle ((kummerInd σ hdeg a r hr s hs) q.1, (kummerInd σ hdeg a r hr s hs) q.2)) ⋯ ⋯

The Evens norm of a Kummer class is the pullback of the D₁₆ class: for a quadratic extension L/K, a ∈ Lˣ, a square root r of σ a and any s ∉ galoisSubgroup K L σ, N^{Ev}((a)) ∈ H²(G_K, 𝔽₂) is the class of the 2-cocycle c_{D₁₆} ∘ (ρ_a × ρ_a), where ρ_a = kummerInd σ hdeg a r hr s hs and c_{D₁₆} = wreathD16Cocycle.