The direct norm-index calculation for odd-valuation radicands #
For a uniformizer radicand, the unit norms meet exactly q ^ v_K(2) square classes,
whereas all units meet 2 * q ^ v_K(2) square classes. Since every square is a norm,
this gives index two on units. The norm of the square-root generator has valuation one,
so the unit quotient is already the full norm quotient.
Rescaling the radicand by a square gives the same result for every odd-valuation radicand, including negative valuations. This proof uses only arithmetic in the base field: it does not use the norm-index theorem, Hilbert-symbol bimultiplicativity, or the square-class count of a quadratic extension.
References #
- O. T. O'Meara, Introduction to Quadratic Forms, §63A.
theorem
TauCeti.quadraticNormSubgroup_index_eq_two_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)))
:
For a radicand of odd normalized valuation, the quadratic norm subgroup has index two.