The Hilbert symbol of a unit and a uniformizer

Over a nonarchimedean local field of odd residue characteristic, the Hilbert symbol of an integral unit and a uniformizer is the quadratic character of the unit's residue. The unramified quadratic class detects the nonsquare residue class, while squares have positive symbol. This calculation is one of the three values determining the local symbol on square classes.

References

• J.-P. Serre, A Course in Arithmetic, Chapter III, §1, Theorem 1.
• O. T. O'Meara, Introduction to Quadratic Forms, §63:11.

@[instance_reducible]

noncomputable def TauCeti.instFintypeResidueField {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Fintype (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The residue field is finite for the quadratic character calculation.

theorem TauCeti.hilbertSymbol_unit_eq_ite_of_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) (u : (↥(ValuativeRel.valuation K).integer)ˣ) {b : Kˣ} (hb : Odd (Multiplicative.toAdd ((normalizedValuation K) b))) : hilbertSymbol ((Units.map ↑(ValuativeRel.valuation K).integer.subtype) u) b = if IsSquare ((Units.map ↑(IsLocalRing.residue ↥(ValuativeRel.valuation K).integer)) u) then 1 else -1

The symbol of a unit and an element of odd valuation is positive exactly when the unit has square residue, in odd residue characteristic.

theorem TauCeti.hilbertSymbol_unit_eq_quadraticChar_of_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) (u : (↥(ValuativeRel.valuation K).integer)ˣ) {b : Kˣ} (hb : Odd (Multiplicative.toAdd ((normalizedValuation K) b))) : ↑(hilbertSymbol ((Units.map ↑(ValuativeRel.valuation K).integer.subtype) u) b) = (quadraticChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ↑((Units.map ↑(IsLocalRing.residue ↥(ValuativeRel.valuation K).integer)) u)

The unit–odd-valuation symbol equals the quadratic residue character of the reduced unit.

theorem TauCeti.hilbertSymbol_unit_uniformizer_eq_ite {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) (u : (↥(ValuativeRel.valuation K).integer)ˣ) {π : Kˣ} (hπ : IsUniformizer K π) : hilbertSymbol ((Units.map ↑(ValuativeRel.valuation K).integer.subtype) u) π = if IsSquare ((Units.map ↑(IsLocalRing.residue ↥(ValuativeRel.valuation K).integer)) u) then 1 else -1

The symbol of a unit and a uniformizer is positive exactly when the unit has square residue. This is the unit–uniformizer entry of the Hilbert-symbol table in odd residue characteristic.

theorem TauCeti.hilbertSymbol_unit_uniformizer_eq_quadraticChar {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) (u : (↥(ValuativeRel.valuation K).integer)ˣ) {π : Kˣ} (hπ : IsUniformizer K π) : ↑(hilbertSymbol ((Units.map ↑(ValuativeRel.valuation K).integer.subtype) u) π) = (quadraticChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ↑((Units.map ↑(IsLocalRing.residue ↥(ValuativeRel.valuation K).integer)) u)

The unit–uniformizer symbol equals the quadratic residue character of the reduced unit.

theorem TauCeti.hilbertSymbol_eq_one_iff_isSquare_of_valuation_zero_of_isUniformizer {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) {u π : Kˣ} (hu : Multiplicative.toAdd ((normalizedValuation K) u) = 0) (hπ : IsUniformizer K π) : hilbertSymbol u π = 1 ↔ IsSquare u

For a valuation-zero element of Kˣ, the unit–uniformizer symbol is positive exactly when that element is a square, in odd residue characteristic.

noncomputable def TauCeti.Units.oddResidueSign {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (u : (↥(ValuativeRel.valuation K).integer)ˣ) : ℤˣ

The sign of the quadratic character of the reduction of an integral unit.

theorem TauCeti.Units.oddResidueSign_eq_one_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (u : (↥(ValuativeRel.valuation K).integer)ˣ) : oddResidueSign u = 1 ↔ IsSquare ((Units.map ↑(IsLocalRing.residue ↥(ValuativeRel.valuation K).integer)) u)

The sign is one exactly when the reduced unit is a square.

theorem TauCeti.Units.oddResidueSign_int {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (u : (↥(ValuativeRel.valuation K).integer)ˣ) : ↑(oddResidueSign u) = (quadraticChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ↑((Units.map ↑(IsLocalRing.residue ↥(ValuativeRel.valuation K).integer)) u)

As an integer, the residue sign is the usual quadratic character.

@[simp]

theorem TauCeti.Units.oddResidueSign_mul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (u v : (↥(ValuativeRel.valuation K).integer)ˣ) : oddResidueSign (u * v) = oddResidueSign u * oddResidueSign v

The residue sign is multiplicative on integral units.

@[simp]

theorem TauCeti.Units.oddResidueSign_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : oddResidueSign 1 = 1

The residue sign of one is one.

@[simp]

theorem TauCeti.Units.oddResidueSign_inv {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (u : (↥(ValuativeRel.valuation K).integer)ˣ) : oddResidueSign u⁻¹ = (oddResidueSign u)⁻¹

The residue sign of an inverse is the inverse sign.

@[simp]

theorem TauCeti.Units.oddResidueSign_zpow {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (u : (↥(ValuativeRel.valuation K).integer)ˣ) (n : ℤ) : oddResidueSign (u ^ n) = oddResidueSign u ^ n

The residue sign of an integer power is the corresponding power of the sign.

theorem TauCeti.oddResidueSign_eq_hilbertSymbol {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) (u : (↥(ValuativeRel.valuation K).integer)ˣ) {π : Kˣ} (hπ : IsUniformizer K π) : Units.oddResidueSign u = hilbertSymbol ((Units.map ↑(ValuativeRel.valuation K).integer.subtype) u) π

The sign is the Hilbert symbol against any uniformizer.

theorem TauCeti.oddResidueSign_neg_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) : Units.oddResidueSign (-1) = (-1) ^ ((Fintype.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) - 1) / 2)

The uniformizer diagonal sign is (-1)^((q-1)/2), where q is the residue cardinality.