The unramified quadratic class of a local field

Let K be a nonarchimedean local field with 2 ≠ 0. This file produces the square class of the unramified quadratic extension in norm-equation form: a unit Δ of 𝒪[K] such that b ∈ Kˣ is a norm from K(√Δ), that is b = x² - Δ y² for some x y : K, exactly when the normalized valuation v_K(b) is even. Equivalently, every unit is a norm and a uniformizer is not. No extension of K is constructed; the statement is about the binary form x² - Δ y² over K.

The class is explicit. Choose c ∈ 𝒪[K] whose residue is not of the form t² + t in the finite residue field 𝓀[K]; such a residue exists because the Artin–Schreier map t ↦ t² + t identifies 0 and -1. Then Δ = 1 + 4c. Since 2 is invertible,

x² - (1 + 4c) y² = (x - y)² + (x - y)(2y) - c (2y)²,

so the norm equation for Δ is the one for the norm form x² + xy - cy² of QuadraticAlgebra 𝒪[K] c 1, the ring 𝒪[K][ω] with ω² = c + ω. Its reduction x² + xy - residue(c)y² is anisotropic over 𝓀[K] by the choice of c. Hence a value of the form at a primitive integral vector is a unit, and every value has even valuation. Conversely the residue norm form is the norm of the quadratic extension of the finite field 𝓀[K], which is surjective, and Hensel's lemma for the norm (TauCeti.Algebra.exists_norm_eq_of_norm_sub_mem, with the unit ω of unit trace 1) lifts it to every unit of 𝒪[K]. The argument does not distinguish odd from even residue characteristic. In odd residue characteristic Δ is a unit with nonsquare residue, and over ℚ₂ the choice c = -1 gives Δ = -3, in the square class of 5.

With the Hilbert symbol this reads (Δ, b)_K = (-1)^{v_K(b)}.

Main results

• TauCeti.exists_eq_sq_sub_one_add_four_mul_mul_sq_iff_even: for c as above, b is a norm from K(√(1 + 4c)) exactly when v_K(b) is even.
• TauCeti.exists_unramified_class: there is a nonsquare Δ of valuation zero whose norms are exactly the elements of even valuation, with valuation K (Δ - 1) ≤ valuation K 4.
• TauCeti.not_isSquare_of_unramified_class: every class with this norm criterion is nonsquare.
• TauCeti.unramified_class_of_isSquare_mul: the criterion is invariant under square classes.
• TauCeti.hilbertSymbol_unramified: for such a Δ, (Δ, b)_K = (-1)^{v_K(b)}.
• TauCeti.hilbertSymbol_two_unramified: for such a Δ, (2, Δ)_K = (-1)^{v_K(2)}.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63A.
• J.-P. Serre, Local Fields, Chapter V, §2.

theorem TauCeti.exists_eq_sq_sub_one_add_four_mul_mul_sq_iff_even {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {c : ↥(ValuativeRel.valuation K).integer} (hc : ∀ (t : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer), t ^ 2 + t ≠ (IsLocalRing.residue ↥(ValuativeRel.valuation K).integer) c) (b : Kˣ) : (∃ (x : K) (y : K), ↑b = x ^ 2 - (1 + 4 * ↑c) * y ^ 2) ↔ Even (Multiplicative.toAdd ((normalizedValuation K) b))

The unramified quadratic class, explicitly. Let c ∈ 𝒪[K] have residue outside the image of t ↦ t² + t. Then b ∈ Kˣ is a norm from K(√(1 + 4c)), that is b = x² - (1 + 4c) y² for some x y : K, exactly when v_K(b) is even.

theorem TauCeti.exists_unramified_class {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : ∃ (Δ : Kˣ), ¬IsSquare Δ ∧ Multiplicative.toAdd ((normalizedValuation K) Δ) = 0 ∧ (ValuativeRel.valuation K) (↑Δ - 1) ≤ (ValuativeRel.valuation K) 4 ∧ ∀ (b : Kˣ), (∃ (x : K) (y : K), ↑b = x ^ 2 - ↑Δ * y ^ 2) ↔ Even (Multiplicative.toAdd ((normalizedValuation K) b))

The unramified quadratic class. There is a nonsquare Δ ∈ Kˣ of valuation zero such that b ∈ Kˣ is a norm from K(√Δ), that is b = x² - Δ y² for some x y : K, exactly when v_K(b) is even. The representative satisfies valuation K ((Δ : K) - 1) ≤ valuation K 4, that is, Δ ≡ 1 mod 4.

theorem TauCeti.not_isSquare_of_unramified_class {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} (ha : ∀ (b : Kˣ), (∃ (x : K) (y : K), ↑b = x ^ 2 - ↑a * y ^ 2) ↔ Even (Multiplicative.toAdd ((normalizedValuation K) b))) : ¬IsSquare a

If the norms from K(√a) are exactly the elements of even normalized valuation, then a is not a square.

theorem TauCeti.unramified_class_of_isSquare_mul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a Δ : Kˣ} (h : IsSquare (a * Δ)) (hΔ : ∀ (b : Kˣ), (∃ (x : K) (y : K), ↑b = x ^ 2 - ↑Δ * y ^ 2) ↔ Even (Multiplicative.toAdd ((normalizedValuation K) b))) (b : Kˣ) : (∃ (x : K) (y : K), ↑b = x ^ 2 - ↑a * y ^ 2) ↔ Even (Multiplicative.toAdd ((normalizedValuation K) b))

The norm criterion only depends on the square class of a.

theorem TauCeti.hilbertSymbol_unramified {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Δ : Kˣ} (hΔ : ∀ (b : Kˣ), (∃ (x : K) (y : K), ↑b = x ^ 2 - ↑Δ * y ^ 2) ↔ Even (Multiplicative.toAdd ((normalizedValuation K) b))) (b : Kˣ) : hilbertSymbol Δ b = if Even (Multiplicative.toAdd ((normalizedValuation K) b)) then 1 else -1

Evaluation against the unramified class. If the norms from K(√Δ) are exactly the elements of even valuation, as for the class of TauCeti.exists_unramified_class, then (Δ, b)_K = (-1)^{v_K(b)}.

theorem TauCeti.hilbertSymbol_two_unramified {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Invertible 2] {Δ : Kˣ} (hΔ : ∀ (b : Kˣ), (∃ (x : K) (y : K), ↑b = x ^ 2 - ↑Δ * y ^ 2) ↔ Even (Multiplicative.toAdd ((normalizedValuation K) b))) : hilbertSymbol (unitOfInvertible 2) Δ = (-1) ^ dyadicLevel K ⋯

The Hilbert symbol of 2 against the unramified class is (2, Δ)_K = (-1)^{v_K(2)}, where v_K(2) is the dyadic level TauCeti.dyadicLevel. In odd residue characteristic it is 1; over a finite extension of ℚ₂ it is -1 exactly when the absolute ramification index is odd.