The number of square classes of a finite extension of a local field

Let K be a nonarchimedean local field with 2 ≠ 0 and let M be a field that is a finite extension of K. A nonarchimedean local field F has 4 · #𝓀[F] ^ v_F(2) square classes (TauCeti.card_squareClass). Equipping M with its local-field structure (TauCeti.algebraicExtensionValuativeRel), the fundamental identity e · f = [M : K] and v_M(2) = e · v_K(2) turn this into a count expressed in terms of K and the degree alone:

#(Mˣ/(Mˣ)²) = 4 · (#𝓀[K] ^ v_K(2)) ^ [M : K].

The statement puts no structure on M beyond that of a finite K-algebra, since the square-class group of a field depends only on the field.

Main results

• TauCeti.card_squareClass_eq_four_mul_pow_finrank: the count above.
• TauCeti.natCard_squareClassGroup_eq_four_mul_pow_finrank: the same count for the additive TauCeti.SquareClassGroup.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §63A.
• J. Neukirch, Algebraic Number Theory, Chapter II, §5 and §6.

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

The number of square classes of a finite extension. If M is a finite extension of a nonarchimedean local field K in which 2 ≠ 0, then Mˣ ⧸ (Mˣ)² has 4 · (#𝓀[K] ^ v_K(2)) ^ [M : K] elements.

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

The number of square classes of a finite extension, read on the additive TauCeti.SquareClassGroup: 4 · (#𝓀[K] ^ v_K(2)) ^ [M : K].