Square classes of a local field with odd residue characteristic #
When two is invertible in the ring of integers of a nonarchimedean local field, its four square
classes are represented by 1, a unit with nonsquare residue, a uniformizer, and their product.
This description supplies the coordinates used to compute the Hilbert symbol in odd residue
characteristic. The residue square test and the count of four square classes come from the local
field power subgroup theory.
References #
- O. T. O'Meara, Introduction to Quadratic Forms, §63, for local square classes and the Hilbert symbol.
theorem
TauCeti.exists_integerUnit_not_isSquare_residue
{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)
At odd residue characteristic there is an integer unit whose residue is nonsquare.
theorem
TauCeti.not_isSquare_integerUnit_mul_uniformizer
{K : Type u_1}
[Field K]
[ValuativeRel K]
[TopologicalSpace K]
[IsNonarchimedeanLocalField K]
(u : (↥(ValuativeRel.valuation K).integer)ˣ)
{π : Kˣ}
(hπ : IsUniformizer K π)
:
Multiplying an integer unit by a uniformizer gives another nonsquare class.
theorem
TauCeti.squareClass_eq_representative_of_isUnit_two
{K : Type u_1}
[Field K]
[ValuativeRel K]
[TopologicalSpace K]
[IsNonarchimedeanLocalField K]
(h2 : IsUnit 2)
(u : (↥(ValuativeRel.valuation K).integer)ˣ)
(hu : ¬IsSquare ((Units.map ↑(IsLocalRing.residue ↥(ValuativeRel.valuation K).integer)) u))
{π : Kˣ}
(hπ : IsUniformizer K π)
(a : Kˣ)
:
squareClass a = 0 ∨ squareClass a = squareClass ((Units.map ↑(ValuativeRel.valuation K).integer.subtype) u) ∨ squareClass a = squareClass π ∨ squareClass a = squareClass ((Units.map ↑(ValuativeRel.valuation K).integer.subtype) u * π)
The four square classes at odd residue characteristic. If u has nonsquare
residue and π is any uniformizer, the classes of 1, u, π, and uπ exhaust the
square-class group.