Square classes in the uniformizer norm family

Let K be a nonarchimedean local field of characteristic different from two. For an irreducible π in the ring of integers, the unit norms from K(√π) have the form u² (1 - π t²). Two parameters s, t give the same square class precisely when they are congruent modulo (2), or equivalently modulo the v_K(2)-th power of the maximal ideal. This separates the parameters in the finite residue quotient used to count the unit norm classes, including in residue characteristic two. ncard_range_uniformizerNormSquareClass computes their number as q ^ v_K(2), and mem_range_uniformizerNormSquareClass_iff identifies the counted range with unit norms.

The proof uses the sharp local square theorem and the obstruction to a square differing from one to odd order below 2 v_K(2).

References

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

theorem TauCeti.valuation_one_sub_uniformizer_mul_sq {K : Type u_1} [Field K] [ValuativeRel K] {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (t : ↥(ValuativeRel.valuation K).integer) : (ValuativeRel.valuation K) (1 - ↑π * ↑t ^ 2) = 1

The values 1 - π t² of the uniformizer norm family have valuation one.

theorem TauCeti.one_sub_uniformizer_mul_sq_ne_zero {K : Type u_1} [Field K] [ValuativeRel K] {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (t : ↥(ValuativeRel.valuation K).integer) : 1 - ↑π * ↑t ^ 2 ≠ 0

A value of the uniformizer norm family is nonzero.

theorem TauCeti.isSquare_div_one_sub_uniformizer_mul_sq_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (s t : ↥(ValuativeRel.valuation K).integer) : IsSquare ((1 - ↑π * ↑t ^ 2) / (1 - ↑π * ↑s ^ 2)) ↔ (ValuativeRel.valuation K) (↑t - ↑s) ≤ (ValuativeRel.valuation K) 2

Two members of the uniformizer norm family differ by a square exactly when their parameters differ by an element of valuation at least v_K(2).

theorem TauCeti.isSquare_div_one_sub_uniformizer_mul_sq_iff_sub_mem {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (s t : ↥(ValuativeRel.valuation K).integer) : IsSquare ((1 - ↑π * ↑t ^ 2) / (1 - ↑π * ↑s ^ 2)) ↔ t - s ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ natCastValuation K 2 h2

Equality of the square classes in the uniformizer norm family is congruence modulo 𝓂[K] ^ v_K(2). This includes odd residue characteristic, when that quotient is trivial.

noncomputable def TauCeti.uniformizerNormSquareClass (K : Type u_2) [Field K] [ValuativeRel K] {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (t : ↥(ValuativeRel.valuation K).integer) : MultiplicativeSquareClassGroup K

The square class of the unit norm 1 - π t², for a uniformizer π.

theorem TauCeti.uniformizerNormSquareClass_def {K : Type u_1} [Field K] [ValuativeRel K] {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (t : ↥(ValuativeRel.valuation K).integer) : uniformizerNormSquareClass K hπ t = squareClassHom (Units.mk0 (1 - ↑π * ↑t ^ 2) ⋯)

The uniformizer norm square class is computed by the native square-class quotient map.

@[simp]

theorem TauCeti.uniformizerNormSquareClass_eq_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (s t : ↥(ValuativeRel.valuation K).integer) : uniformizerNormSquareClass K hπ t = uniformizerNormSquareClass K hπ s ↔ t - s ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ natCastValuation K 2 h2

The parameter of a uniformizer norm square class is determined modulo 𝓂[K] ^ v_K(2).

theorem TauCeti.mem_range_uniformizerNormSquareClass_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (c : MultiplicativeSquareClassGroup K) : c ∈ Set.range (uniformizerNormSquareClass K hπ) ↔ ∃ (b : Kˣ), (ValuativeRel.valuation K) ↑b = 1 ∧ b ∈ quadraticNormSubgroup ↑π ∧ squareClassHom b = c

The range of the uniformizer norm family consists exactly of the square classes of unit norms. The norm condition uses the quadratic algebra with radicand π.

theorem TauCeti.ncard_range_uniformizerNormSquareClass {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) : (Set.range (uniformizerNormSquareClass K hπ)).ncard = Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ natCastValuation K 2 h2

The uniformizer norm family meets exactly q ^ v_K(2) square classes, where q is the residue-field cardinality.