The Hasse norm principle fails for ℚ(√13, √17)

The cyclic Hasse norm theorem TauCeti.ClassFieldTheory.isGlobalNorm_iff_isLocalNormEverywhere says that for a cyclic extension a local norm everywhere is a global norm. This file records the standard counterexample showing that the cyclic hypothesis cannot be dropped: for the biquadratic field L = ℚ(√13, √17), whose Galois group is (ℤ/2)², the number 25 is a local norm everywhere (isLocalNormEverywhere_twentyFive) but not a norm from L (twentyFive_notMem_normGroup).

The local half holds because Gal(L/ℚ) has exponent two, so every square of ℚˣ, and in particular 25 = 5², is a local norm everywhere by TauCeti.ClassFieldTheory.isLocalNormEverywhere_pow_of_exponent_dvd.

The global half is proved by Hilbert reciprocity over ℚ. Let F = ℚ(√13) and suppose that 25 = N_{L/ℚ}(x). Then y = N_{L/F}(x) has norm 25 from F, so Hilbert's Theorem 90 for F/ℚ, made explicit, writes y m = 5 z² with z ∈ F and m = c² - 13 d² a nonzero norm from F. Hence q = 5 m is a norm from L = F(√17) down to F, say q = α² - 17 β² with α, β ∈ F. At every place ℓ where 13 is a square, an embedding of F into ℚ_ℓ turns this into a solution of q = x² - 17 y², so the Hilbert symbol (17, q)_ℓ is 1. At the remaining places the symbol is computed from Legendre symbols: there (13, m)_ℓ = 1 forces (17, m)_ℓ = 1, so (17, q)_ℓ = (17, 5)_ℓ, which is 1 except at ℓ = 5, where it is (17 / 5) = -1. So the product of the symbols (17, q)_v over all places is -1, contradicting Hilbert's product formula TauCeti.finprod_hilbertSymbol_padic_mul_hilbertSymbol_real_eq_one.

The field is described by square roots s of 13 and t of 17 that generate it; no particular model of ℚ(√13, √17) is chosen.

Main results

• TauCeti.ClassFieldTheory.isLocalNormEverywhere_twentyFive: 25 is a norm at every place of ℚ from the local étale algebras of ℚ(√13, √17).
• TauCeti.ClassFieldTheory.twentyFive_notMem_normGroup: 25 is not a norm from ℚ(√13, √17).

References

• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Exercise 5.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §4.
• J.-P. Serre, A Course in Arithmetic, Chapter III, §2 (Hilbert's product formula).

The local computation behind the global half

Computations in ℚ(√13)

The counterexample

theorem TauCeti.ClassFieldTheory.isLocalNormEverywhere_twentyFive {L : Type u_1} [Field L] [NumberField L] {s t : L} (hs : s ^ 2 = 13) (ht : t ^ 2 = 17) (hst : ℚ⟮s, t⟯ = ⊤) : GlobalNumberFields.IsLocalNormEverywhere ℚ L (Units.mk0 25 isLocalNormEverywhere_twentyFive._proof_1)

25 is a local norm everywhere from ℚ(√13, √17). If L is generated over ℚ by square roots s of 13 and t of 17, then 25 is a norm from the local étale algebra ℚ_v ⊗[ℚ] L at every finite and infinite place v of ℚ.

theorem TauCeti.ClassFieldTheory.twentyFive_notMem_normGroup {L : Type u_1} [Field L] [NumberField L] {s t : L} (hs : s ^ 2 = 13) (ht : t ^ 2 = 17) (hst : ℚ⟮s, t⟯ = ⊤) : Units.mk0 25 isLocalNormEverywhere_twentyFive._proof_1 ∉ normGroup ℚ L

25 is not a norm from ℚ(√13, √17). If L is generated over ℚ by square roots s of 13 and t of 17, then 25 is not the norm of an element of L. Together with isLocalNormEverywhere_twentyFive this shows that the Hasse norm principle fails for the biquadratic extension L/ℚ.