Unit square classes of a local field

The image of the integer-ring units in Kˣ / (Kˣ)² consists exactly of the classes of even normalized valuation. The valuation modulo two descends to a surjective homomorphism on square classes, with this image as its kernel. Consequently the unit square classes have index two, including in residue characteristic two. They are also the image of the depth-zero unit filtration U(K, 0), so their number is the relative index of the squares in U(K, 0).

This subgroup is the intended comparison target for the almost-everywhere reference images of the standard integral special orthogonal family in dimension at least three. Its index distinguishes it from the whole square-class group; a uniformizer never belongs to it. The construction is independent of a uniformizer, although a uniformizer gives a splitting of the valuation homomorphism.

All groups use their canonical topologies.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63A and §101.
• J.-P. Serre, A Course in Arithmetic, Chapter II, §3.

noncomputable def TauCeti.unitSquareClasses (K : Type u_1) [Field K] [ValuativeRel K] : Subgroup (Kˣ ⧸ Subgroup.square Kˣ)

The subgroup of square classes represented by units of the ring of integers.

theorem TauCeti.mem_unitSquareClasses_iff (K : Type u_1) [Field K] [ValuativeRel K] (c : Kˣ ⧸ Subgroup.square Kˣ) : c ∈ unitSquareClasses K ↔ ∃ (u : (↥(ValuativeRel.valuation K).integer)ˣ), (QuotientGroup.mk' (Subgroup.square Kˣ)) ((Units.map ↑(ValuativeRel.valuation K).integer.subtype) u) = c

Membership in the unit square classes means having an integer-unit representative.

noncomputable def TauCeti.squareClassValuation (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Kˣ ⧸ Subgroup.square Kˣ →* Multiplicative (ZMod 2)

Normalized valuation modulo two, descended to the multiplicative square-class quotient.

@[simp]

theorem TauCeti.squareClassValuation_mk (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) : (squareClassValuation K) ↑a = Multiplicative.ofAdd ↑(Multiplicative.toAdd ((normalizedValuation K) a))

The valuation of a square class is the normalized valuation of a representative modulo two.

theorem TauCeti.squareClassValuation_surjective (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Function.Surjective ⇑(squareClassValuation K)

The valuation map on square classes is surjective.

@[simp]

theorem TauCeti.mk_mem_unitSquareClasses_iff (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : Kˣ) : ↑a ∈ unitSquareClasses K ↔ Even (Multiplicative.toAdd ((normalizedValuation K) a))

A unit of the field has an integer-unit square-class representative exactly when its normalized valuation is even.

theorem TauCeti.unitSquareClasses_eq_ker_squareClassValuation (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : unitSquareClasses K = (squareClassValuation K).ker

Unit square classes are the kernel of valuation modulo two.

@[simp]

theorem TauCeti.unitSquareClasses_index (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (unitSquareClasses K).index = 2

The unit square classes have index two in every nonarchimedean local field.

theorem TauCeti.mk_notMem_unitSquareClasses_of_isUniformizer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {π : Kˣ} (hπ : IsUniformizer K π) : (QuotientGroup.mk' (Subgroup.square Kˣ)) π ∉ unitSquareClasses K

A uniformizer's class does not belong to the unit square classes.

theorem TauCeti.unitSquareClasses_ne_top (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : unitSquareClasses K ≠ ⊤

Unit square classes are a proper subgroup, also in residue characteristic two.

theorem TauCeti.isOpen_unitSquareClasses (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsOpen ↑(unitSquareClasses K)

The unit square classes are open in the local square-class quotient.

theorem TauCeti.card_unitSquareClasses (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : Nat.card ↥(unitSquareClasses K) = 2 * Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ natCastValuation K 2 h2

When two is nonzero, the number of unit square classes is twice the residue-field cardinality raised to the normalized valuation of two.

theorem TauCeti.card_unitSquareClasses_of_isUnit_two (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) : Nat.card ↥(unitSquareClasses K) = 2

Away from residue characteristic two, there are two unit square classes.

theorem TauCeti.card_unitSquareClasses_dyadic (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [FinitePadicExtension K 2] : Nat.card ↥(unitSquareClasses K) = 2 * Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ absoluteRamificationIndex K 2

A finite compatible extension of ℚ₂ has 2 · #𝓀[K] ^ e(K/ℚ₂) unit square classes.

theorem TauCeti.map_unitFiltration_zero_eq_unitSquareClasses (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Subgroup.map (QuotientGroup.mk' (Subgroup.square Kˣ)) (unitFiltration K 0) = unitSquareClasses K

The unit square classes are the image of U(K, 0), the units of valuation one, in the square-class quotient.

theorem TauCeti.relIndex_square_unitFiltration_zero (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : (Subgroup.square Kˣ).relIndex (unitFiltration K 0) = 2 * Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ natCastValuation K 2 h2

When two is nonzero, U(K, 0) has 2 · q ^ v_K(2) classes modulo the squares of Kˣ, where q is the cardinality of the residue field.

theorem TauCeti.unitSquareClasses_padic_eq_range (p : ℕ) [Fact (Nat.Prime p)] : unitSquareClasses ℚ_[p] = ((QuotientGroup.mk' (Subgroup.square ℚ_[p]ˣ)).comp (Units.map ↑PadicInt.Coe.ringHom)).range

Over ℚ_p, the unit square classes are exactly the image of ℤ_pˣ in the square-class quotient, using the usual inclusion of the p-adic integers.

@[simp]

theorem TauCeti.mk_mem_unitSquareClasses_padic_iff (p : ℕ) [Fact (Nat.Prime p)] (a : ℚ_[p]ˣ) : ↑a ∈ unitSquareClasses ℚ_[p] ↔ Even (↑a).valuation

For p-adic fields the unit square-class test is the parity of the usual p-adic valuation.

theorem TauCeti.card_unitSquareClasses_padic_two : Nat.card ↥(unitSquareClasses ℚ_[2]) = 4

The dyadic field ℚ₂ has four unit square classes, rather than two.