The frame of an orthogonal basis of the transferred plane

Let L/K be a separable quadratic extension, σ : L → Kˢ a K-embedding, s ∈ G_K outside G_L = galoisSubgroup K L σ, a ∈ Lˣ, and r ∈ Kˢ a square root of σ(a). The map φ(y) = (σ(y) r, s(σ(y) r)) (TauCeti.kummerPoint) realizes the transferred form Tr_*⟨a⟩ inside (Kˢ)², and g ∈ G_K acts on its coordinates by ρ_a(g)ᵀ, where ρ_a is the signed-permutation representation of TauCeti.kummerInd.

Let (y₀, y₁) be an orthogonal basis of Tr_*⟨a⟩ with values w_j = Tr_{L/K}(a y_j²), and choose square roots c_j ∈ Kˢ of w_j. The matrix P whose j-th column is φ(y_j)/c_j (TauCeti.kummerFrame) is orthogonal, and

P⁻¹ ρ_a(g) g(P) = diag((−1)^{rootSign c₀ g}, (−1)^{rootSign c₁ g})

(TauCeti.kummerFrame_conj). In other words, in Z¹(G_K, O₂(Kˢ)) the cocycle ρ_a is cohomologous to the diagonal cocycle of the Kummer characters of w₀ and w₁. This is the diagonalization step of Serre's computation of the Evens norm of a Kummer class.

Main definitions

• TauCeti.kummerFrame: the matrix whose j-th column is φ(y_j)/c_j.

Main results

• TauCeti.kummerFrame_mem_orthogonalGroup: the frame of an orthogonal basis, normalized by square roots of its values, is an orthogonal matrix.
• TauCeti.wreathSignedPerm_kummerInd_mul_map_kummerFrame: ρ_a(g) g(P) = P D(g) for the diagonal sign matrix D(g) of the Kummer characters of the values.
• TauCeti.kummerFrame_conj: P is orthogonal and P⁻¹ ρ_a(g) g(P) = D(g).

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.kummerFrame {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (r : SeparableClosure K) (s : AbsoluteGaloisGroup K) (y : Fin 2 → L) (c : Fin 2 → SeparableClosure K) : Matrix (Fin 2) (Fin 2) (SeparableClosure K)

The frame of a basis of the transferred plane: for y : Fin 2 → L and c : Fin 2 → Kˢ, the matrix whose j-th column is φ(y_j) / c_j, where φ = kummerPoint σ r s.

@[simp]

theorem TauCeti.kummerFrame_apply {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L] (σ : L →ₐ[K] SeparableClosure K) (r : SeparableClosure K) (s : AbsoluteGaloisGroup K) (y : Fin 2 → L) (c : Fin 2 → SeparableClosure K) (i j : Fin 2) : kummerFrame σ r s y c i j = (kummerPoint σ r s) (y j) i / c j

The (i, j) entry of the frame is the i-th coordinate of φ(y_j) / c_j.

theorem TauCeti.kummerFrame_mem_orthogonalGroup {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 : Fin 2 → L} (hy : (Algebra.trace K L) (a * y 0 * y 1) = 0) {c : Fin 2 → SeparableClosure K} (hc : ∀ (i : Fin 2), c i ^ 2 = (algebraMap K (SeparableClosure K)) ((Algebra.trace K L) (a * y i ^ 2))) (hc0 : ∀ (i : Fin 2), c i ≠ 0) : kummerFrame σ r s y c ∈ Matrix.orthogonalGroup (Fin 2) (SeparableClosure K)

The frame of an orthogonal basis is orthogonal. If Tr_{L/K}(a y₀ y₁) = 0 and c_j² = Tr_{L/K}(a y_j²) with c_j ≠ 0, then the columns φ(y_j) / c_j are orthonormal for the unit form of (Kˢ)².

theorem TauCeti.wreathSignedPerm_kummerInd_mul_map_kummerFrame {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 : Fin 2 → L) {c : Fin 2 → SeparableClosure K} {w : Fin 2 → K} (hc : ∀ (i : Fin 2), c i ^ 2 = (algebraMap K (SeparableClosure K)) (w i)) (g : AbsoluteGaloisGroup K) : wreathSignedPerm ((kummerInd σ hdeg a r hr s hs) g) * (kummerFrame σ r s y c).map ⇑g = kummerFrame σ r s y c * Matrix.diagonal fun (i : Fin 2) => (-1) ^ (rootSign (c i) g).val

The frame turns ρ_a into a diagonal cocycle: ρ_a(g) g(P) = P D(g), where P is the frame of y normalized by elements c_j whose squares lie in K, and D(g) = diag((−1)^{rootSign c₀ g}, (−1)^{rootSign c₁ g}). No orthogonality of y and no nonvanishing of c is needed for this identity.

theorem TauCeti.kummerFrame_conj {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 : Fin 2 → L) (hy : (Algebra.trace K L) (↑a * y 0 * y 1) = 0) (c : Fin 2 → SeparableClosure K) (hc : ∀ (i : Fin 2), c i ^ 2 = (algebraMap K (SeparableClosure K)) ((Algebra.trace K L) (↑a * y i ^ 2))) (hc0 : ∀ (i : Fin 2), c i ≠ 0) (g : AbsoluteGaloisGroup K) : kummerFrame σ r s y c ∈ Matrix.orthogonalGroup (Fin 2) (SeparableClosure K) ∧ (kummerFrame σ r s y c)⁻¹ * wreathSignedPerm ((kummerInd σ hdeg a r hr s hs) g) * (kummerFrame σ r s y c).map ⇑g = Matrix.diagonal fun (i : Fin 2) => (-1) ^ (rootSign (c i) g).val

The diagonalization of ρ_a. Let y be an orthogonal basis of Tr_*⟨a⟩, with values w_j = Tr_{L/K}(a y_j²), and let c_j ∈ Kˢ be nonzero with c_j² = w_j. Then the frame P of y normalized by c is orthogonal and P⁻¹ ρ_a(g) g(P) = diag((−1)^{rootSign c₀ g}, (−1)^{rootSign c₁ g}): in Z¹(G_K, O₂(Kˢ)) the cocycle ρ_a = wreathSignedPerm ∘ kummerInd is cohomologous to the diagonal cocycle of the Kummer characters of w₀ and w₁.