Norm valuations from a radicand of odd quadratic defect #
An optimal square approximation to a nonsquare a gives a norm from K(√a) whose valuation is
the defect exponent of a: if a - ξ² = x, then ξ² - a = -x is the norm of ξ + √a.
If the defect exponent is odd, multiplying this norm by a square gives valuation one; its
integer powers then give norms of every integer valuation. This identifies the valuation part
of the norm group in the ramified unit case of the local Hilbert symbol.
References #
- O. T. O'Meara, Introduction to Quadratic Forms, §63A.
theorem
TauCeti.exists_mem_quadraticNormSubgroup_toAdd_normalizedValuation_eq_of_odd_defectExponent
{K : Type u_1}
[Field K]
[ValuativeRel K]
[TopologicalSpace K]
[IsNonarchimedeanLocalField K]
{a : Kˣ}
{d : ℤ}
(hd : defectExponent a = ↑d)
(hodd : Odd d)
(n : ℤ)
:
∃ b ∈ quadraticNormSubgroup ↑a, Multiplicative.toAdd ((normalizedValuation K) b) = n
If the defect exponent is odd, every integer is the valuation of a quadratic norm.