The quadratic norm index through square classes

Let K be a field with 2 ≠ 0, let a : Kˣ be a nonsquare, and let L = K(√a) be the quadratic algebra QuadraticAlgebra K a 0, which is then a field. The inclusion Kˣ → Lˣ and the norm Lˣ → Kˣ induce homomorphisms of square-class groups

Kˣ/(Kˣ)² → Lˣ/(Lˣ)² → Kˣ/(Kˣ)².

The first has kernel {1, [a]}, because an element of K that is a square in L has the form x² or a y² with x, y ∈ K. Its image is the kernel of the second, which is the quadratic case of Hilbert's Theorem 90: an element w of norm one is either -1, which lies in K, or u / ū = u² / N(u) with u = 1 + w. The image of the second map is the image of the norm subgroup N = N_{L/K}(Lˣ), which contains the squares. Counting the three groups gives

2 · (Kˣ : N) · #(Lˣ/(Lˣ)²) = #(Kˣ/(Kˣ)²)².

No finiteness is assumed: indices and cardinalities are Subgroup.index and Nat.card, which are 0 for infinite groups. Over a field whose two square-class groups are finite and known, such as a nonarchimedean local field in which 2 ≠ 0, the identity determines the index of the norm subgroup.

Main results

• TauCeti.two_mul_index_quadraticNormSubgroup_mul_card_squareClass: the identity above.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Chapter VII, §3, for the exact sequence of square-class groups of a quadratic extension.

theorem TauCeti.two_mul_index_quadraticNormSubgroup_mul_card_squareClass {K : Type u_1} [Field K] (a : Kˣ) [Fact ¬IsSquare ↑a] (h2 : 2 ≠ 0) : 2 * (quadraticNormSubgroup ↑a).index * Nat.card (MultiplicativeSquareClassGroup (QuadraticAlgebra K (↑a) 0)) = Nat.card (MultiplicativeSquareClassGroup K) ^ 2

The norm index of a quadratic extension through square classes. If 2 ≠ 0 in K and a : Kˣ is not a square, then 2 · (Kˣ : N) · #(Lˣ/(Lˣ)²) = #(Kˣ/(Kˣ)²)², where L = K(√a) and N is the subgroup of norms from L.