The number of square classes of a nonarchimedean local field

Let K be a nonarchimedean local field with normalized valuation v_K and uniformizer π. If K is a finite extension of ℚ_[2], then

#(Kˣ/(Kˣ)²) = 4 · #𝓀[K] ^ e(K/ℚ_[2]).

In particular ℚ_[2] has eight square classes. Away from residue characteristic two the square-class group has four elements, and for a nonsquare u of even valuation the four classes are represented by

1, u, π, u π.

The choice of u is part of the statement. Up to squares u is a unit of 𝒪[K], and by TauCeti.isSquare_unitsMap_subtype_iff such a unit is a nonsquare exactly when its residue is a nonsquare of 𝓀[K]. The theorem TauCeti.exists_mem_unitFiltration_not_isSquare supplies a nonsquare in the unit filtration whenever K has characteristic different from two. This is the list of representatives used to compute Hilbert symbols over K and to count its quadratic extensions.

Main results

• TauCeti.card_squareClass and TauCeti.natCard_squareClassGroup: if 2 is nonzero, there are 4 · #𝓀[K] ^ v_K(2) square classes. These read the count TauCeti.card_squareClasses on Kˣ ⧸ (powMonoidHom 2).range on the literal quotient by squares and on the square-class group.
• TauCeti.card_squareClasses_dyadic: a finite extension of ℚ_[2] has 4 · #𝓀[K] ^ e(K/ℚ_[2]) square classes.
• TauCeti.card_squareClass_dyadic and TauCeti.natCard_squareClassGroup_dyadic: the same count on the literal quotient by squares and on the square-class group.
• TauCeti.card_squareClasses_padic_two: ℚ_[2] has eight square classes.
• TauCeti.card_squareClass_of_odd: away from residue characteristic two the literal quotient by squares has four elements.
• TauCeti.natCard_squareClassGroup_of_isUnit_two: away from residue characteristic two the square-class group has four elements.
• TauCeti.isAddKleinFour_squareClassGroup_of_isUnit_two: away from residue characteristic two the square-class group is a Klein four-group.
• TauCeti.squareClass_ne_zero_and_ne_of_isUniformizer_of_even_of_not_isSquare: the four specified square classes are pairwise distinct.
• TauCeti.eq_zero_or_eq_squareClass_of_isUnit_two: the four specified square classes exhaust the square-class group.
• TauCeti.exists_isSquare_mul_of_isUnit_two: every element of Kˣ agrees, up to a square, with one of 1, u, π, u π.
• TauCeti.exists_isSquare_mul_of_integerUnit_residue_not_isSquare: the four representatives can be formed from any specified integer-ring unit with nonsquare residue.
• TauCeti.isSquare_or_isSquare_mul_of_isUnit_two: an element of even valuation is a square or u times a square.

References

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

@[simp]

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

The multiplicative square-class group of a nonarchimedean local field. This is TauCeti.card_squareClasses read on the literal quotient Kˣ ⧸ (Kˣ)².

@[simp]

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

The square-class group of a nonarchimedean local field. This is TauCeti.card_squareClasses read on TauCeti.SquareClassGroup.

@[simp]

theorem TauCeti.card_squareClasses_dyadic {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [FinitePadicExtension K 2] : Nat.card (Kˣ ⧸ (powMonoidHom 2).range) = 4 * Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ absoluteRamificationIndex K 2

The number of square classes of a dyadic local field. If K is a finite compatible extension of ℚ_[2], then Kˣ ⧸ (Kˣ)² has 4 · #𝓀[K] ^ e(K/ℚ_[2]) elements.

@[simp]

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

The multiplicative square-class group of a dyadic local field. This is TauCeti.card_squareClasses_dyadic read on the literal quotient Kˣ ⧸ (Kˣ)²; TauCeti.natCard_squareClassGroup_dyadic restates it on the additive TauCeti.SquareClassGroup.

@[simp]

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

The square-class group of a dyadic local field. This is the count #(Kˣ ⧸ (Kˣ)²) = 4 · #𝓀[K] ^ e(K/ℚ_[2]) of TauCeti.card_squareClasses_dyadic, read on TauCeti.SquareClassGroup.

theorem TauCeti.card_squareClasses_padic_two : Nat.card (ℚ_[2]ˣ ⧸ (powMonoidHom 2).range) = 8

The multiplicative group of ℚ_[2] has eight square classes.

@[simp]

theorem TauCeti.card_squareClass_of_odd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) : Nat.card (MultiplicativeSquareClassGroup K) = 4

The multiplicative square-class group of a nonarchimedean local field away from residue characteristic two has four elements. This is the literal quotient Kˣ ⧸ (Kˣ)²; TauCeti.natCard_squareClassGroup_of_isUnit_two restates it on the additive TauCeti.SquareClassGroup.

@[simp]

theorem TauCeti.natCard_squareClassGroup_of_isUnit_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) : Nat.card (SquareClassGroup K) = 4

The square-class group of a nonarchimedean local field away from residue characteristic two has four elements. This is the count #(Kˣ ⧸ (Kˣ)²) = 4 of TauCeti.card_squareClasses_of_isUnit, read on TauCeti.SquareClassGroup.

theorem TauCeti.isAddKleinFour_squareClassGroup_of_isUnit_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) : IsAddKleinFour (SquareClassGroup K)

Away from residue characteristic two, the square-class group of a nonarchimedean local field is a Klein four-group.

theorem TauCeti.squareClass_ne_zero_and_ne_of_isUniformizer_of_even_of_not_isSquare {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {u π : Kˣ} (hπ : IsUniformizer K π) (hu : Even (Multiplicative.toAdd ((normalizedValuation K) u))) (hu' : ¬IsSquare u) : squareClass u ≠ 0 ∧ squareClass π ≠ 0 ∧ squareClass (u * π) ≠ 0 ∧ squareClass u ≠ squareClass π ∧ squareClass u ≠ squareClass (u * π) ∧ squareClass π ≠ squareClass (u * π)

For a nonsquare u of even valuation and a uniformizer π, the square classes of 1, u, π, and u * π are pairwise distinct.

theorem TauCeti.eq_zero_or_eq_squareClass_of_isUnit_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) {π u : Kˣ} (hπ : IsUniformizer K π) (hu : Even (Multiplicative.toAdd ((normalizedValuation K) u))) (hu' : ¬IsSquare u) (x : SquareClassGroup K) : x = 0 ∨ x = squareClass u ∨ x = squareClass π ∨ x = squareClass (u * π)

The four square classes of a nonarchimedean local field of odd residue characteristic. For a nonsquare u of even valuation and a uniformizer π, their four classes exhaust the square-class group.

theorem TauCeti.exists_isSquare_mul_of_isUnit_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) {π u : Kˣ} (hπ : IsUniformizer K π) (hu : Even (Multiplicative.toAdd ((normalizedValuation K) u))) (hu' : ¬IsSquare u) (a : Kˣ) : ∃ r ∈ {1, u, π, u * π}, IsSquare (a * r)

The four square classes of a nonarchimedean local field of odd residue characteristic. For a uniformizer π and a nonsquare u of even valuation, every element of Kˣ becomes a square after multiplication by one of 1, u, π, u π. Together with TauCeti.natCard_squareClassGroup_of_isUnit_two this says that the four listed elements represent the four square classes. The choice of representatives follows TauCetiRoadmap/QuadraticFormInvariants/README.md.

theorem TauCeti.exists_isSquare_mul_of_integerUnit_residue_not_isSquare {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {π : Kˣ} (hπ : IsUniformizer K π) (u : (↥(ValuativeRel.valuation K).integer)ˣ) (hu : ¬IsSquare ((Units.map ↑(IsLocalRing.residue ↥(ValuativeRel.valuation K).integer)) u)) (a : Kˣ) : ∃ r ∈ {1, (Units.map ↑(ValuativeRel.valuation K).integer.subtype) u, π, (Units.map ↑(ValuativeRel.valuation K).integer.subtype) u * π}, IsSquare (a * r)

The four square classes with an explicitly chosen unramified unit. If a unit u of 𝒪[K] has nonsquare residue (which forces odd residue characteristic), then every element of Kˣ agrees, up to a square, with one of 1, u, π, and u π.

theorem TauCeti.isSquare_or_isSquare_mul_of_isUnit_two {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : IsUnit 2) {u w : Kˣ} (hu : Even (Multiplicative.toAdd ((normalizedValuation K) u))) (hu' : ¬IsSquare u) (hw : Even (Multiplicative.toAdd ((normalizedValuation K) w))) : IsSquare w ∨ IsSquare (w * u)

The even-valuation square classes away from residue characteristic two. An element of even valuation is a square, or u times a square, for any fixed nonsquare u of even valuation.