Deep units are squares, at the sharp depth

In a nonarchimedean local field of characteristic different from two, every unit in U(K, 2 v_K(2) + 1) is a square. The resulting openness of the square subgroup, including in residue characteristic two, is proved in PowerSubgroup.Open and supplies neighborhoods in which a nonzero value stays in one square class.

The exponent is natCastValuation K 2 h2, so no choice of a dyadic base field is needed. The inclusion is the case p = 2, i = v_K(2) + 1 of TauCeti.map_powMonoidHom_unitFiltration_of_prime: squaring carries U(K, v_K(2) + 1) onto U(K, 2 v_K(2) + 1).

The depth is sharp: U(K, 2 v_K(2)) is not contained in the squares. Since 𝓂[K]^(2 v_K(2)) = 4 𝒪[K], an element 1 + 4c of that depth is a square exactly when c = t² + t for some integral t, so any c whose residue lies outside the image of the Artin–Schreier map t ↦ t² + t of 𝓀[K] gives a non-square. That map identifies 0 and -1, so on the finite residue field it is not surjective. The argument is uniform in the residue characteristic: when it is odd, v_K(2) = 0 and the statement is that some unit is not a square.

Main results

• TauCeti.unitFiltration_le_range_powMonoidHom_two: U(K, 2 v_K(2) + 1) ⊆ (Kˣ)².
• TauCeti.isSquare_of_eq_one_add_four_mul: a residue Artin–Schreier condition makes 1 + 4m a square.
• TauCeti.valuation_one_add_four_mul: in residue characteristic two, 1 + 4m is a unit.
• TauCeti.not_mem_range_of_eq_sq_mul_one_add_four_mul: a nonsquare of the form ζ² (1 + 4m) has residue of m outside the Artin–Schreier range.
• TauCeti.not_unitFiltration_le_range_powMonoidHom_two: U(K, 2 v_K(2)) ⊄ (Kˣ)².
• TauCeti.exists_mem_unitFiltration_not_isSquare: a nonsquare witness in U(K, 2 v_K(2)).
• TauCeti.unitFiltration_le_range_powMonoidHom_two_iff: U(K, n) ⊆ (Kˣ)² exactly when 2 v_K(2) + 1 ≤ n.
• TauCeti.dyadicLevel: the valuation v_K(2) used in the square interface.
• TauCeti.unitFiltration_le_square and TauCeti.not_unitFiltration_le_square: the same sharp square theorem expressed using Subgroup.square Kˣ.
• TauCeti.valuation_sq_sub_one_ne_pow_odd and TauCeti.not_isSquare_one_add_pow_odd: below depth 2 v_K(2), a square cannot differ from one to exact odd order, so 1 + π^(2k+1) is not a square when k < v_K(2).
• TauCeti.exists_integerUnit_residue_not_isSquare: away from residue characteristic two there is a unit of 𝒪[K] whose residue is a nonsquare.
• TauCeti.isSquare_zpow_mul_iff: for w of even valuation, π ^ m * w is a square exactly when m is even and w is a square.
• TauCeti.not_isSquare_mul_of_isUniformizer_of_even_toAdd_normalizedValuation: a uniformizer times an element of even valuation is not a square.
• TauCeti.not_isSquare_of_isUniformizer: a uniformizer is not a square.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63A, local square theorem.
• J. Neukirch, Algebraic Number Theory, Chapter II, §5.
• J.-P. Serre, A Course in Arithmetic, Chapter II, §3, for the case K = ℚ₂.

noncomputable def TauCeti.dyadicLevel (K : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : ℕ

The dyadic level v_K(2), expressed using the supplied natural-valued valuation.

@[simp]

theorem TauCeti.dyadicLevel_def {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : dyadicLevel K h2 = natCastValuation K 2 h2

theorem TauCeti.span_four_eq_maximalIdeal_pow {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : Ideal.span {4} = IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ (2 * natCastValuation K 2 h2)

In characteristic different from two, the ideal (4) of 𝒪[K] is 𝓂[K] ^ (2 v_K(2)).

theorem TauCeti.valuation_four_eq_pow {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) : (ValuativeRel.valuation K) 4 = (ValuativeRel.valuation K) ↑π ^ (2 * natCastValuation K 2 h2)

In characteristic different from two, the valuation of 4 is that of π ^ (2 v_K(2)), for an irreducible element π of 𝒪[K].

theorem TauCeti.unitFiltration_le_range_powMonoidHom_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : unitFiltration K (2 * natCastValuation K 2 h2 + 1) ≤ (powMonoidHom 2).range

Every unit of depth 2 v_K(2) + 1 is a square. This includes dyadic local fields; only characteristic two itself is excluded.

theorem TauCeti.isSquare_of_eq_one_add_four_mul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {w : Kˣ} {m : ↥(ValuativeRel.valuation K).integer} (hw : ↑w = 1 + 4 * ↑m) (hwv : (ValuativeRel.valuation K) ↑w = 1) (hm : (IsLocalRing.residue ↥(ValuativeRel.valuation K).integer) m ∈ Set.range fun (t : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) => t ^ 2 + t) : IsSquare w

A unit w = 1 + 4m is a square if the residue of m lies in the range of t ↦ t² + t.

@[simp]

theorem TauCeti.valuation_one_add_four_mul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) (he : 0 < natCastValuation K 2 h2) (n : ↥(ValuativeRel.valuation K).integer) : (ValuativeRel.valuation K) (1 + 4 * ↑n) = 1

In residue characteristic two, 4 ∈ 𝓂[K], so every 1 + 4n with n ∈ 𝒪[K] is a unit.

theorem TauCeti.not_mem_range_of_eq_sq_mul_one_add_four_mul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) (he : 0 < natCastValuation K 2 h2) {a ζ : Kˣ} {n : ↥(ValuativeRel.valuation K).integer} (ha : ¬IsSquare a) (hn : ↑a = ↑ζ ^ 2 * (1 + 4 * ↑n)) : (IsLocalRing.residue ↥(ValuativeRel.valuation K).integer) n ∉ Set.range fun (t : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) => t ^ 2 + t

In residue characteristic two, if a nonsquare is ζ² (1 + 4n) with n ∈ 𝒪[K], the residue of n lies outside the range of t ↦ t² + t.

theorem TauCeti.not_unitFiltration_le_range_powMonoidHom_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : ¬unitFiltration K (2 * natCastValuation K 2 h2) ≤ (powMonoidHom 2).range

The local square theorem is sharp: not every unit of depth 2 v_K(2) is a square. In residue characteristic two the witness is 1 + 4c for any c whose residue is not of the form t² + t; for K = ℚ₂ this says that 5 ∈ 1 + 4ℤ₂ is not a square. In odd residue characteristic the depth is zero and the statement is that some unit is not a square.

theorem TauCeti.exists_mem_unitFiltration_not_isSquare {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : ∃ u ∈ unitFiltration K (2 * natCastValuation K 2 h2), ¬IsSquare u

There is a nonsquare in the last unit-filtration step not entirely contained in the squares.

theorem TauCeti.unitFiltration_le_square {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : unitFiltration K (2 * dyadicLevel K h2 + 1) ≤ Subgroup.square Kˣ

Every unit of depth 2 * dyadicLevel K + 1 is a square.

theorem TauCeti.not_unitFiltration_le_square {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : ¬unitFiltration K (2 * dyadicLevel K h2) ≤ Subgroup.square Kˣ

The sharp depth cannot be decreased: units at 2 * dyadicLevel K are not all squares.

theorem TauCeti.unitFiltration_le_range_powMonoidHom_two_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {n : ℕ} : unitFiltration K n ≤ (powMonoidHom 2).range ↔ 2 * natCastValuation K 2 h2 + 1 ≤ n

The exact depth of the local square theorem: U(K, n) consists of squares if and only if n ≥ 2 v_K(2) + 1.

theorem TauCeti.valuation_sq_sub_one_ne_pow_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) {k : ℕ} (hk : k < natCastValuation K 2 h2) (ξ : K) : (ValuativeRel.valuation K) (ξ ^ 2 - 1) ≠ (ValuativeRel.valuation K) ↑π ^ (2 * k + 1)

Below twice the valuation of two, a square cannot differ from one to exact odd order.

theorem TauCeti.not_isSquare_one_add_pow_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) {k : ℕ} (hk : k < natCastValuation K 2 h2) : ¬IsSquare (Units.mk0 (1 + ↑π ^ (2 * k + 1)) ⋯)

For k < v_K(2), the unit represented by 1 + π^(2k+1) is not a square.

theorem TauCeti.isSquare_zpow_mul_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {π w : Kˣ} (hπ : IsUniformizer K π) (hw : Even (Multiplicative.toAdd ((normalizedValuation K) w))) (m : ℤ) : IsSquare (π ^ m * w) ↔ Even m ∧ IsSquare w

Squares in a nonarchimedean local field. Written against a uniformizer π, an element π ^ m * w with w of even valuation is a square exactly when m is even and w is a square. No hypothesis on the residue characteristic is needed.

theorem TauCeti.not_isSquare_mul_of_isUniformizer_of_even_toAdd_normalizedValuation {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {π w : Kˣ} (hπ : IsUniformizer K π) (hw : Even (Multiplicative.toAdd ((normalizedValuation K) w))) : ¬IsSquare (π * w)

A uniformizer times an element of even valuation has odd valuation, so it is not a square.

theorem TauCeti.not_isSquare_of_isUniformizer {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {π : Kˣ} (hπ : IsUniformizer K π) : ¬IsSquare π

A uniformizer is not a square.

theorem TauCeti.exists_integerUnit_residue_not_isSquare {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) : ∃ (u : (↥(ValuativeRel.valuation K).integer)ˣ), ¬IsSquare ((Units.map ↑(IsLocalRing.residue ↥(ValuativeRel.valuation K).integer)) u)

Away from residue characteristic two, there is a unit of 𝒪[K] whose residue is a nonsquare.