Quadratic norms for a radicand of odd valuation

Let K be a nonarchimedean local field with 2 ≠ 0, and let a ∈ Kˣ have odd normalized valuation v_K(a), so that K(√a)/K is ramified. This file exhibits an explicit non-norm from K(√a), in every residue characteristic. If Δ is the unramified class, whose norms are exactly the elements of even valuation (TauCeti.exists_unramified_class), then (Δ, a)_K = (-1)^{v_K(a)} = -1, and by symmetry (a, Δ)_K = -1. So Δ, a unit, is not a norm from K(√a). This is the explicit witness for the nondegeneracy of the Hilbert symbol at a radicand of odd valuation.

Main results

• TauCeti.hilbertSymbol_eq_neg_one_of_unramified_class_of_odd: (a, Δ)_K = -1 for the unramified class Δ.
• TauCeti.exists_hilbertSymbol_eq_neg_one_of_odd: there is a b ∈ Kˣ of valuation zero, the unramified class, with (a, b)_K = -1.

The index theorem for every nonsquare radicand, and the resulting bimultiplicativity of the Hilbert symbol, are in TauCeti.NumberTheory.LocalField.QuadraticForm.Bimultiplicativity.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63A.
• J.-P. Serre, A Course in Arithmetic, Chapter III, §1.

theorem TauCeti.hilbertSymbol_eq_neg_one_of_unramified_class_of_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {a Δ : Kˣ} (hΔ : ∀ (b : Kˣ), (∃ (x : K) (y : K), ↑b = x ^ 2 - ↑Δ * y ^ 2) ↔ Even (Multiplicative.toAdd ((normalizedValuation K) b))) (ha : Odd (Multiplicative.toAdd ((normalizedValuation K) a))) : hilbertSymbol a Δ = -1

An odd-valuation radicand against the unramified class. If v_K(a) is odd and the norms from K(√Δ) are exactly the elements of even valuation, as for the class of TauCeti.exists_unramified_class, then (a, Δ)_K = -1.

theorem TauCeti.exists_hilbertSymbol_eq_neg_one_of_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {a : Kˣ} (ha : Odd (Multiplicative.toAdd ((normalizedValuation K) a))) : ∃ (b : Kˣ), Multiplicative.toAdd ((normalizedValuation K) b) = 0 ∧ hilbertSymbol a b = -1

Nondegeneracy for a radicand of odd valuation. If v_K(a) is odd, there is b ∈ Kˣ of valuation zero with (a, b)_K = -1, namely the unramified class.