The Galois action on the transferred plane

Let L/K be a quadratic extension, σ : L → Kˢ a K-embedding, a ∈ Lˣ with a square root r² = σ(a), and s ∈ G_K outside G_L = galoisSubgroup K L σ. The transferred plane is realized inside (Kˢ)² by the Kummer points φ(y) = (σ(y) r, s(σ(y) r)) (TauCeti.kummerPoint), whose dot product is the twisted trace pairing (TauCeti.kummerPoint_dotProduct).

This file computes the action of G_K on these points coordinatewise: it is given by the transpose of the signed-permutation matrix of ρ_a = Ind α_a : G_K → C₂ ≀ C₂ (TauCeti.kummerInd), the representation induced from the Kummer character α_a of G_L:

g(φ(y)) = ρ_a(g)ᵀ φ(y).

At y = 1 this says that the columns of ρ_a(g) record the images of the roots r and s r of X² − σ(a) and X² − s(σ(a)) under g, in the basis (r, s r). The map g ↦ ρ_a(g)ᵀ is an anti-homomorphism, while ρ_a itself is a homomorphism. This is the representation through which the Evens norm of the Kummer class of a is computed, by diagonalizing ρ_a in an orthogonal basis of the transferred form.

Main results

• TauCeti.kummerPoint_galois: g(φ(y)) = ρ_a(g)ᵀ φ(y).

References

• J.-P. Serre, L'invariant de Witt de la forme Tr(x²), Comment. Math. Helv. 59 (1984), 651–676, second proof of Théorème 1′.
• 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.

theorem TauCeti.kummerPoint_galois {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 σ) (y : L) (g : AbsoluteGaloisGroup K) : (fun (i : Fin 2) => g ((kummerPoint σ r s) y i)) = (wreathSignedPerm ((kummerInd σ hdeg a r hr s hs) g)).transpose.mulVec ((kummerPoint σ r s) y)

The Galois action on the transferred plane is the transpose of the induced Kummer representation: for g ∈ G_K, applying g to the coordinates of the Kummer point φ(y) = (σ(y) r, s(σ(y) r)) gives ρ_a(g)ᵀ φ(y), where ρ_a = kummerInd σ hdeg a r hr s hs acts on (Kˢ)² by signed permutations.