The quadratic defect

Let K be a nonarchimedean local field with ring of integers 𝒪[K]. The quadratic defect of a : Kˣ is O'Meara's fractional ideal

𝔡(a) = ⋂_{ξ ∈ K} (a - ξ²) 𝒪[K],

which measures how well a can be approximated by squares of K. Its exponent is δ(a) = sup_{ξ ∈ K} v_K(a - ξ²) ∈ ℤ ∪ {⊤} for the normalized valuation v_K.

FractionalIdeal is a lattice without infima of infinite families, so the defect is defined as the greatest lower bound of the principal fractional ideals (a - ξ²) 𝒪[K], and TauCeti.isGLB_quadraticDefect records that property. The infimum is attained: the approximation orders v_K(a - ξ²) of a nonsquare are bounded, because a sequence of better and better approximations would have a common point in the compact closed ball of radius max 1 (valuation K a), giving a square root of a. Consequently the defect of a nonsquare is the principal fractional ideal 𝓂[K] ^ δ(a), while the defect of a square is 0 and its exponent is ⊤.

The results here are the calculus of the defect used to compute Hilbert symbols over K: the defect vanishes exactly on squares, it scales by c² when a is multiplied by c², the defect of an integral element is integral, and the defect of an element of odd valuation v_K(a) is a 𝒪[K]. None of that needs a hypothesis on the residue characteristic.

The classification below additionally assumes (2 : K) ≠ 0. For e = v_K(2) and a unit u, 𝔡(u) runs through the list 0, 4 𝒪[K] = 𝓂[K]^{2e}, and 𝓂[K]^{2k+1} for 0 ≤ k < e, with the value 0 occurring exactly when u is a square. If u is not a square, δ(u) is 2e or an odd number below 2e. The upper bound is the sharp local square theorem, and the parity is an approximation argument: below depth 2e the cross term 2 ξ π^k s is negligible, so an approximation of even order can always be improved using that the residue field is perfect of characteristic two. Every listed value is attained: sharpness supplies the value 2e, and 1 + π^(2k+1) has defect exponent 2k+1. Every nonsquare radicand, including one of negative valuation, has a square multiple that is a uniformizer or a unit of maximal or positive odd defect.

Main definitions

• TauCeti.quadraticDefect: the quadratic defect 𝔡(a), a fractional ideal of 𝒪[K].
• TauCeti.defectExponent: its exponent δ(a) : WithTop ℤ.

Main results

• TauCeti.isGLB_quadraticDefect: 𝔡(a) is the greatest lower bound of the ideals (a - ξ²) 𝒪[K], and TauCeti.exists_quadraticDefect_eq_spanSingleton: it is one of them.
• TauCeti.quadraticDefect_eq_zero_iff and TauCeti.defectExponent_eq_top_iff: the defect detects squares.
• TauCeti.quadraticDefect_eq_maximalIdeal_zpow: 𝔡(a) = 𝓂[K] ^ δ(a) for a nonsquare a, and TauCeti.quadraticDefect_eq_spanSingleton_of_defectExponent_eq: 𝔡(a) = c 𝒪[K] whenever v_K(c) = δ(a).
• TauCeti.quadraticDefect_mul_sq and TauCeti.defectExponent_mul_sq: behaviour under multiplication by a square.
• TauCeti.quadraticDefect_of_odd and TauCeti.defectExponent_of_odd: the defect of an element of odd valuation.
• TauCeti.defectExponent_le_two_mul_natCastValuation: the defect exponent of a nonsquare unit is at most 2 v_K(2).
• TauCeti.dyadicLevel_ne_zero_of_defectExponent_eq: a unit of positive defect exponent forces v_K(2) ≠ 0.
• TauCeti.defectExponent_eq_two_mul_natCastValuation_or_odd and TauCeti.quadraticDefect_eq_maximalIdeal_zpow_or_odd: the possible defects of a unit.
• TauCeti.exists_mul_sq_cases_of_not_isSquare: the three-case normalization of a nonsquare radicand, with an explicit square-rescaling witness.
• TauCeti.exists_unit_defectExponent_eq_two_mul_natCastValuation and TauCeti.defectExponent_one_add_pow_odd: every entry in that list is attained, with an explicit representative for each odd exponent.
• TauCeti.defectExponent_eq_two_mul_natCastValuation_of_mem_unitFiltration: every nonsquare in U(K, 2 v_K(2)) has the maximal defect exponent 2 v_K(2).

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63A, in particular 63:1 and 63:2.

noncomputable def TauCeti.defectExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) : WithTop ℤ

The defect exponent δ(a) = sup_{ξ ∈ K} v_K(a - ξ²) of a : Kˣ, where v_K is the normalized valuation. It is ⊤ exactly when a is a square; otherwise the supremum is attained, see TauCeti.exists_defectExponent_eq.

@[simp]

theorem TauCeti.defectExponent_eq_top_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} : defectExponent a = ⊤ ↔ IsSquare a

The defect exponent is ⊤ exactly on squares.

theorem TauCeti.not_isSquare_of_defectExponent_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} {d : ℤ} (hd : defectExponent a = ↑d) : ¬IsSquare a

A unit with finite defect exponent is not a square.

theorem TauCeti.notMem_range_algebraMap_of_defectExponent_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type u_2} [Field L] [Algebra K L] {a : Kˣ} {x : L} (hx2 : x ^ 2 = (algebraMap K L) ↑a) {d : ℤ} (hd : defectExponent a = ↑d) : x ∉ Set.range ⇑(algebraMap K L)

A square root x of a unit a with finite defect exponent does not lie in the base field, since a is not a square.

theorem TauCeti.le_defectExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) (ξ : K) (x : Kˣ) (hx : ↑x = ↑a - ξ ^ 2) : ↑(Multiplicative.toAdd ((normalizedValuation K) x)) ≤ defectExponent a

Every approximation order v_K(a - ξ²) is at most the defect exponent.

theorem TauCeti.exists_defectExponent_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} (ha : ¬IsSquare a) : ∃ (ξ : K) (x : Kˣ), ↑x = ↑a - ξ ^ 2 ∧ ↑(Multiplicative.toAdd ((normalizedValuation K) x)) = defectExponent a

The defect exponent of a nonsquare is attained by some approximation ξ² of a.

theorem TauCeti.toAdd_normalizedValuation_le_defectExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) : ↑(Multiplicative.toAdd ((normalizedValuation K) a)) ≤ defectExponent a

The valuation of a is at most its defect exponent, by the approximation ξ = 0.

noncomputable def TauCeti.quadraticDefect {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) : FractionalIdeal (nonZeroDivisors ↥(ValuativeRel.valuation K).integer) K

The quadratic defect 𝔡(a) = ⋂_{ξ ∈ K} (a - ξ²) 𝒪[K] of a : Kˣ, the greatest fractional ideal of 𝒪[K] contained in every principal fractional ideal (a - ξ²) 𝒪[K].

theorem TauCeti.isGLB_quadraticDefect {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) : IsGLB (Set.range fun (ξ : K) => (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) (↑a - ξ ^ 2)) (quadraticDefect a)

The quadratic defect is the greatest lower bound of the principal fractional ideals (a - ξ²) 𝒪[K].

theorem TauCeti.quadraticDefect_le {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) (ξ : K) : quadraticDefect a ≤ (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) (↑a - ξ ^ 2)

The quadratic defect is contained in every (a - ξ²) 𝒪[K].

theorem TauCeti.le_quadraticDefect {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} {I : FractionalIdeal (nonZeroDivisors ↥(ValuativeRel.valuation K).integer) K} (h : ∀ (ξ : K), I ≤ (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) (↑a - ξ ^ 2)) : I ≤ quadraticDefect a

A fractional ideal contained in every (a - ξ²) 𝒪[K] is contained in the quadratic defect.

theorem TauCeti.quadraticDefect_eq_spanSingleton_of_forall {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} {ξ₀ : K} (h : ∀ (ξ : K), (ValuativeRel.valuation K) (↑a - ξ₀ ^ 2) ≤ (ValuativeRel.valuation K) (↑a - ξ ^ 2)) : quadraticDefect a = (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) (↑a - ξ₀ ^ 2)

If a - ξ₀² has the smallest valuation among the a - ξ², the quadratic defect is (a - ξ₀²) 𝒪[K].

theorem TauCeti.exists_quadraticDefect_eq_spanSingleton {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) : ∃ (ξ : K), quadraticDefect a = (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) (↑a - ξ ^ 2)

The infimum defining the quadratic defect is attained: 𝔡(a) = (a - ξ²) 𝒪[K] for some ξ ∈ K.

@[simp]

theorem TauCeti.quadraticDefect_eq_zero_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} : quadraticDefect a = 0 ↔ IsSquare a

The quadratic defect vanishes exactly on squares.

theorem TauCeti.quadraticDefect_le_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} (ha : ↑a ∈ (ValuativeRel.valuation K).integer) : quadraticDefect a ≤ 1

The quadratic defect of an integral element is an integral ideal.

theorem TauCeti.quadraticDefect_mul_sq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a c : Kˣ) : quadraticDefect (a * c ^ 2) = (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) (↑c ^ 2) * quadraticDefect a

Multiplying a by the square c² multiplies its quadratic defect by c².

theorem TauCeti.defectExponent_mul_sq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a c : Kˣ) : defectExponent (a * c ^ 2) = defectExponent a + ↑(2 * Multiplicative.toAdd ((normalizedValuation K) c))

Multiplying a by the square c² shifts its defect exponent by 2 v_K(c).

theorem TauCeti.exists_defectExponent_mul_sq_eq_sub_of_even_valuation {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} {d : ℤ} (hd : defectExponent a = ↑d) (ha : Even (Multiplicative.toAdd ((normalizedValuation K) a))) : ∃ (c : Kˣ), (ValuativeRel.valuation K) ↑(a * c ^ 2) = 1 ∧ defectExponent (a * c ^ 2) = ↑(d - Multiplicative.toAdd ((normalizedValuation K) a))

An element of even valuation and finite defect exponent d has a square multiple that is a unit with defect exponent d - v_K(a), even when v_K(a) is negative.

theorem TauCeti.defectExponent_of_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} (ha : Odd (Multiplicative.toAdd ((normalizedValuation K) a))) : defectExponent a = ↑(Multiplicative.toAdd ((normalizedValuation K) a))

The defect exponent of an element of odd valuation is its valuation.

theorem TauCeti.quadraticDefect_of_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} (ha : Odd (Multiplicative.toAdd ((normalizedValuation K) a))) : quadraticDefect a = (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) ↑a

The quadratic defect of an element a of odd valuation is a 𝒪[K].

theorem TauCeti.quadraticDefect_eq_maximalIdeal_zpow {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : Kˣ} {n : ℤ} (h : defectExponent a = ↑n) : quadraticDefect a = ↑(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ^ n

The quadratic defect of a nonsquare is 𝓂[K] ^ δ(a), for its defect exponent δ(a).

theorem TauCeti.quadraticDefect_eq_spanSingleton_of_defectExponent_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a c : Kˣ} (h : defectExponent a = ↑(Multiplicative.toAdd ((normalizedValuation K) c))) : quadraticDefect a = (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) ↑c

The quadratic defect of a nonsquare is generated by any c whose valuation is the defect exponent δ(a).

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

The improvement step of O'Meara 63:2. In residue characteristic two, an approximation u - ξ² of an integral element u : K of order at least 2k with k < v_K(2) can be improved to order at least 2k + 1: writing (u - ξ²)/π^{2k} ≡ s² mod 𝓂[K], which is possible because the residue field is perfect of characteristic two, gives the correction ξ + π^k s. The hypothesis k < v_K(2) makes the cross term 2 ξ π^k s negligible.

theorem TauCeti.defectExponent_le_two_mul_natCastValuation {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {u : Kˣ} (hu : (ValuativeRel.valuation K) ↑u = 1) (hsq : ¬IsSquare u) : defectExponent u ≤ ↑↑(2 * natCastValuation K 2 h2)

The local square theorem bounds the defect of a unit. A unit of 𝒪[K] approximated by a square to order 2 v_K(2) + 1 is a square, so the defect exponent of a nonsquare unit is at most 2 v_K(2). In odd residue characteristic the bound is 0.

theorem TauCeti.dyadicLevel_ne_zero_of_defectExponent_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {a : Kˣ} (ha : (ValuativeRel.valuation K) ↑a = 1) {d : ℤ} (hd : defectExponent a = ↑d) (hd0 : 0 < d) : dyadicLevel K h2 ≠ 0

A unit of positive defect exponent forces v_K(2) ≠ 0. Its defect exponent is at most 2 v_K(2); in odd residue characteristic every nonsquare unit has defect exponent 0.

theorem TauCeti.defectExponent_eq_two_mul_natCastValuation_or_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {u : Kˣ} (hu : (ValuativeRel.valuation K) ↑u = 1) (hsq : ¬IsSquare u) : defectExponent u = ↑↑(2 * natCastValuation K 2 h2) ∨ ∃ k < natCastValuation K 2 h2, defectExponent u = ↑↑(2 * k + 1)

The possible defects of a unit (O'Meara 63:2). For a unit of 𝒪[K] which is not a square, the defect exponent is either 2 v_K(2) or an odd number below 2 v_K(2); equivalently, by TauCeti.quadraticDefect_eq_maximalIdeal_zpow, the defect is 𝓂[K] ^ (2 v_K(2)) = 4 𝒪[K] or 𝓂[K] ^ (2k+1) with k < v_K(2). In odd residue characteristic the list has the single entry 𝒪[K], and the statement is Hensel's lemma. The defect of a square is 0.

theorem TauCeti.exists_mul_sq_cases_of_not_isSquare {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) (a : Kˣ) (ha : ¬IsSquare a) : ∃ (b : Kˣ) (c : Kˣ), b = a * c ^ 2 ∧ ¬IsSquare b ∧ (IsUniformizer K b ∨ (ValuativeRel.valuation K) ↑b = 1 ∧ (defectExponent b = ↑↑(2 * natCastValuation K 2 h2) ∨ ∃ k < natCastValuation K 2 h2, defectExponent b = ↑↑(2 * k + 1)))

A suitable square multiple of a nonsquare is a nonsquare uniformizer or a unit whose defect exponent is maximal or positive odd. The unit-defect alternatives are bounded by v_K(2), so at odd residue characteristic only the maximal-defect alternative remains.

theorem TauCeti.defectExponent_eq_two_mul_natCastValuation_of_mem_unitFiltration {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {u : Kˣ} (hu : u ∈ unitFiltration K (2 * natCastValuation K 2 h2)) (hnsq : ¬IsSquare u) : defectExponent u = ↑↑(2 * natCastValuation K 2 h2)

A nonsquare in U(K, 2 v_K(2)) has defect exponent exactly 2 v_K(2): it is approximated by 1² to order at least 2 v_K(2), while no nonsquare unit has larger defect exponent.

theorem TauCeti.exists_unit_defectExponent_eq_two_mul_natCastValuation {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : ∃ (u : Kˣ), (ValuativeRel.valuation K) ↑u = 1 ∧ ¬IsSquare u ∧ defectExponent u = ↑↑(2 * natCastValuation K 2 h2)

The maximal finite unit defect is attained. This is the defect-theoretic form of the sharpness of the local square theorem: every nonsquare in U(K, 2 v_K(2)) has defect exponent 2 v_K(2).

theorem TauCeti.defectExponent_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) : defectExponent (Units.mk0 (1 + ↑π ^ (2 * k + 1)) ⋯) = ↑↑(2 * k + 1)

For k < v_K(2), the unit represented by 1 + π^(2k+1) has defect exponent exactly 2k+1.

theorem TauCeti.exists_unit_defectExponent_eq_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {k : ℕ} (hk : k < natCastValuation K 2 h2) : ∃ (u : Kˣ), (ValuativeRel.valuation K) ↑u = 1 ∧ ¬IsSquare u ∧ defectExponent u = ↑↑(2 * k + 1)

Every odd unit defect below the maximal one is attained.

theorem TauCeti.quadraticDefect_eq_maximalIdeal_zpow_or_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {u : Kˣ} (hu : (ValuativeRel.valuation K) ↑u = 1) (hsq : ¬IsSquare u) : quadraticDefect u = ↑(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ^ ↑(2 * natCastValuation K 2 h2) ∨ ∃ k < natCastValuation K 2 h2, quadraticDefect u = ↑(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ^ ↑(2 * k + 1)

The possible defects of a unit, as ideals (O'Meara 63:2). The quadratic defect of a nonsquare unit of 𝒪[K] is 𝓂[K] ^ (2 v_K(2)), which is the ideal 4 𝒪[K] by TauCeti.span_four_eq_maximalIdeal_pow, or 𝓂[K] ^ (2k+1) for some k < v_K(2). With TauCeti.quadraticDefect_eq_zero_iff, which covers the squares, this is the complete list of the defects of units, of length v_K(2) + 2.