The transferred plane inside the separable closure

Let L/K be a separable quadratic extension, let σ : L → Kˢ be a K-embedding, and choose s ∈ G_K outside the subgroup fixing σ(L). For a ∈ L and a square root r² = σ(a), the map

φ(y) = (σ(y) r, s(σ(y) r))

realizes the transferred quadratic plane y ↦ Tr_{L/K}(a y²) inside (Kˢ)²: its standard dot product satisfies

φ(y) · φ(y') = Tr_{L/K}(a y y').

The two coordinates correspond to the two embeddings of the quadratic extension into Kˢ, namely σ and s ∘ σ. This realization is the plane on which the induced Kummer representation acts in the computation of the Evens norm of a Kummer class.

Main definitions

• TauCeti.kummerPoint: the K-linear map y ↦ φ(y) = (σ(y) r, s(σ(y) r)) from L to (Kˢ)².

Main results

• TauCeti.kummerPoint_dotProduct: the standard dot product on the image of φ is the twisted trace pairing (y, y') ↦ Tr_{L/K}(a y 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.

noncomputable def TauCeti.kummerPoint {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (r : SeparableClosure K) (s : AbsoluteGaloisGroup K) : L →ₗ[K] Fin 2 → SeparableClosure K

The point of the transferred plane associated to y ∈ L: φ(y) = (σ(y) r, s(σ(y) r)) ∈ (Kˢ)², bundled as a K-linear map in y. When r² = σ(a) and s represents the nontrivial coset of G_L in G_K, the image of φ carries the transferred form Tr_*⟨a⟩.

theorem TauCeti.kummerPoint_def {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (r : SeparableClosure K) (s : AbsoluteGaloisGroup K) (y : L) : (kummerPoint σ r s) y = ![σ y * r, s (σ y * r)]

kummerPoint σ r s y is the vector ![σ y * r, s (σ y * r)].

@[simp]

theorem TauCeti.kummerPoint_apply_zero {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (r : SeparableClosure K) (s : AbsoluteGaloisGroup K) (y : L) : (kummerPoint σ r s) y 0 = σ y * r

The first coordinate of kummerPoint σ r s y is σ(y) r.

@[simp]

theorem TauCeti.kummerPoint_apply_one {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (r : SeparableClosure K) (s : AbsoluteGaloisGroup K) (y : L) : (kummerPoint σ r s) y 1 = s (σ y * r)

The second coordinate of kummerPoint σ r s y is s(σ(y) r).

theorem TauCeti.kummerPoint_dotProduct {K : Type u} [Field K] {L : Type v} [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 y' : L) : (kummerPoint σ r s) y ⬝ᵥ (kummerPoint σ r s) y' = (algebraMap K (SeparableClosure K)) ((Algebra.trace K L) (a * y * y'))

The transferred-plane identity: if L/K is separable quadratic, r² = σ(a), and s ∈ G_K does not fix σ(L), then φ(y) · φ(y') = Tr_{L/K}(a y y') after embedding into Kˢ.

Thus the standard quadratic form on (Kˢ)², restricted along y ↦ φ(y), is the scalar extension of the trace transfer of the line ⟨a⟩.