Quadratic norms of a uniformizer

For a uniformizer a, the unit norms from K(√a) are exactly u² (1 - a t²) with u a unit of the ring of integers and t integral. More generally every nonzero norm is such a unit norm times an integer power of -a. This reduces the norm-index calculation for a radicand of valuation one to the unit values of a binary quadratic form, including in residue characteristic two.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63A.

theorem TauCeti.valuation_sq_sub_mul_sq_of_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} (ha : Odd (Multiplicative.toAdd ((normalizedValuation K) a))) (x y : K) : (ValuativeRel.valuation K) (x ^ 2 - ↑a * y ^ 2) = max ((ValuativeRel.valuation K) (x ^ 2)) ((ValuativeRel.valuation K) (↑a * y ^ 2))

For an odd-valuation radicand, the terms in a quadratic norm cannot cancel in valuation.

theorem TauCeti.valuation_sq_sub_mul_sq_eq_one_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} (ha : IsUniformizer K a) (x y : K) : (ValuativeRel.valuation K) (x ^ 2 - ↑a * y ^ 2) = 1 ↔ (ValuativeRel.valuation K) x = 1 ∧ (ValuativeRel.valuation K) y ≤ 1

A norm for a uniformizer radicand has valuation zero exactly when its first coordinate is a local unit and its second coordinate is integral.

theorem TauCeti.mem_quadraticNormSubgroup_iff_of_isUniformizer {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a b : Kˣ} (ha : IsUniformizer K a) (hb : (ValuativeRel.valuation K) ↑b = 1) : b ∈ quadraticNormSubgroup ↑a ↔ ∃ (u : (↥(ValuativeRel.valuation K).integer)ˣ) (t : ↥(ValuativeRel.valuation K).integer), ↑b = ↑↑u ^ 2 * (1 - ↑a * ↑t ^ 2)

A local unit is a norm for a uniformizer radicand exactly when it has the form u² (1 - a t²), with u an integral unit and t integral.

theorem TauCeti.mem_quadraticNormSubgroup_iff_exists_zpow_mul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a b : Kˣ} (ha : IsUniformizer K a) : b ∈ quadraticNormSubgroup ↑a ↔ ∃ (n : ℤ) (u : (↥(ValuativeRel.valuation K).integer)ˣ) (t : ↥(ValuativeRel.valuation K).integer), ↑b = (-↑a) ^ n * ↑↑u ^ 2 * (1 - ↑a * ↑t ^ 2)

Every nonzero norm for a uniformizer radicand is an integer power of -a times u² (1 - a t²), and every such element is a norm.