Norms from an algebra containing a square root

Let F be a field in which 2 is invertible, b ∈ Fˣ, and M a commutative F-algebra in which the image of b is a square. Then every norm N_{M/F}(c) of a unit c of M is a norm from the quadratic algebra F[√b], so the norm-equation Hilbert symbol (b, N_{M/F}(c)) is 1. The invertibility of 2 is used only when b is already a square in F: in characteristic two the symbol (1, c) is 1 only for squares c.

When b is a square in F the symbol is 1 outright. Otherwise F[√b] is the field F(√b), and a square root s of b in M makes M an algebra over it by √b ↦ s; transitivity of the norm in the tower F ⊆ F(√b) → M writes N_{M/F}(c) as the norm from F(√b) of N_{M/F(√b)}(c). No finiteness of M over F is needed, since the norm of an algebra that is not module-finite is 1.

Applied to the completions L_w ⊇ K_v of a number field L in which b ∈ Kˣ is a square, it shows that every factor N_{L_w/K_v}(c_w) of a coordinate of an idele norm from L is a norm from K_v(√b). This is how the norm-equation Hilbert symbol sees the idele norm group N_{L/K}(𝕀_L).

Main results

• TauCeti.hilbertSymbol_normUnits_eq_one: if b is a square in M, then (b, N_{M/F}(c)) = 1 for every unit c of M.

References

• O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 71:19a.

@[simp]

theorem TauCeti.hilbertSymbol_normUnits_eq_one {F : Type u_1} {M : Type u_2} [Field F] [Invertible 2] [CommRing M] [Algebra F M] {b : Fˣ} (hb : IsSquare ((algebraMap F M) ↑b)) (c : Mˣ) : hilbertSymbol b ((Algebra.normUnits F) c) = 1

Norms from an algebra containing √b are norms from F(√b). If the image of b ∈ Fˣ in the commutative F-algebra M is a square, then the Hilbert symbol (b, N_{M/F}(c)) is 1 for every unit c of M.