The cyclic Hasse norm theorem

Let L/K be a cyclic extension of number fields with Galois group G generated by g. An element a ∈ Kˣ is a global norm if it lies in N_{L/K}(Lˣ), and a local norm everywhere if its principal idele lies in N_{L/K}(I_L). By TauCeti.GlobalNumberFields.mem_range_ideleNormMap_iff, the latter says that a is a norm from the local étale algebra K_v ⊗_K L at every place v. This file relates the two notions through idele-class H¹.

By two-periodicity of the cohomology of G, the class cyclicClass hg a ∈ H²(G, Lˣ) of a vanishes exactly when a is a global norm (TauCeti.cyclicClass_eq_zero_iff). The same periodicity for the ideles, together with the formula N_{L/K}(x) = ∏_σ σ x for the idele norm (idelesRep_norm_apply), shows that the image of this class in H²(G, I_L) vanishes exactly when a is a local norm everywhere (map_unitsToIdeles_cyclicClass_eq_zero_iff). The long exact sequence of 0 → Lˣ → I_L → C_L → 0 identifies the kernel of H²(G, Lˣ) → H²(G, I_L) with the image of the injective connecting map H¹(G, C_L) → H²(G, Lˣ). Hence a is a local norm everywhere exactly when its class comes from H¹(G, C_L) (unitEmbedding_mem_range_ideleNormMap_iff_cyclicClass_mem_range). Since every class of H²(G, Lˣ) is the class of some a (TauCeti.cyclicClass_surjective), the local norms everywhere modulo the global norms thus correspond to H¹(G, C_L).

In particular H¹(G, C_L) vanishes exactly when every local norm everywhere is a global norm (subsingleton_groupCohomology_one_ideleClassRep_iff_forall_mem_normGroup_of_mem_range).

The vanishing of H¹(G, C_L) holds for every finite Galois extension of number fields, as a consequence of the second fundamental inequality (TauCeti.ClassFieldTheory.subsingleton_groupCohomology_one_ideleClassRep). This gives the cyclic Hasse norm theorem (cyclicHasseNorm): for L/K cyclic, a ∈ Kˣ is a norm from Lˣ exactly when its principal idele is an idele norm from L. Read placewise through TauCeti.GlobalNumberFields.unitEmbedding_mem_range_ideleNormMap_iff, it says that a is a global norm exactly when it is a norm from the local étale algebra K_v ⊗_K L at every finite and every infinite place (isGlobalNorm_iff_isLocalNormEverywhere). The cyclic hypothesis cannot be dropped: in ℚ(√13, √17)/ℚ, whose Galois group is (ℤ/2)², the number 25 is a local norm everywhere but not a global norm (TauCeti.ClassFieldTheory.isLocalNormEverywhere_twentyFive and TauCeti.ClassFieldTheory.twentyFive_notMem_normGroup).

Main results

• map_unitsToIdeles_cyclicClass_eq_zero_iff: the class of a dies in H²(G, I_L) exactly when a is a local norm everywhere.
• unitEmbedding_mem_range_ideleNormMap_iff_cyclicClass_mem_range: a is a local norm everywhere exactly when its class comes from H¹(G, C_L).
• subsingleton_groupCohomology_one_ideleClassRep_iff_forall_mem_normGroup_of_mem_range: H¹(G, C_L) = 0 exactly when every local norm everywhere is a global norm.
• cyclicHasseNorm: the cyclic Hasse norm theorem, in idelic form.
• isGlobalNorm_iff_isLocalNormEverywhere: the cyclic Hasse norm theorem, in terms of the norm equations at all completions.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §4.
• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §2.

@[simp]

theorem TauCeti.ClassFieldTheory.map_unitsToIdeles_cyclicClass_eq_zero_iff {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) (a : Kˣ) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id Gal(L/K)) (unitsToIdeles K L) 2)) ((cyclicClass hg) (Additive.ofMul a)) = 0 ↔ (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) a ∈ (GlobalNumberFields.ideleNormMap K L).range

The class of a dies in H²(G, I_L) exactly when a is a local norm everywhere. For L/K cyclic with generator g, the map H²(Gal(L/K), Lˣ) → H²(Gal(L/K), I_L) induced by the principal ideles sends the class of a ∈ Kˣ to zero exactly when the principal idele of a is an idele norm from L.

theorem TauCeti.ClassFieldTheory.unitEmbedding_mem_range_ideleNormMap_iff_cyclicClass_mem_range {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {g : Gal(L/K)} (hg : ∀ (σ : Gal(L/K)), σ ∈ Subgroup.zpowers g) (a : Kˣ) : (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) a ∈ (GlobalNumberFields.ideleNormMap K L).range ↔ (cyclicClass hg) (Additive.ofMul a) ∈ (ideleClassToUnitsH2 K L).range

Local norms are the classes coming from idele-class H¹. For L/K cyclic with generator g, the principal idele of a ∈ Kˣ is an idele norm from L exactly when the class of a in H²(Gal(L/K), Lˣ) is the image of a class of H¹(Gal(L/K), C_L) under the connecting map of 0 → Lˣ → I_L → C_L → 0.

theorem TauCeti.ClassFieldTheory.subsingleton_groupCohomology_one_ideleClassRep_iff_forall_mem_normGroup_of_mem_range {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] : Subsingleton ↑(groupCohomology (ideleClassRep K L) 1) ↔ ∀ (a : Kˣ), (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) a ∈ (GlobalNumberFields.ideleNormMap K L).range → a ∈ normGroup K L

Idele-class H¹ vanishes exactly when local norms are global norms. For L/K cyclic, H¹(Gal(L/K), C_L) = 0 exactly when every a ∈ Kˣ whose principal idele is an idele norm from L lies in N_{L/K}(Lˣ).

theorem TauCeti.ClassFieldTheory.cyclicHasseNorm (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (a : Kˣ) : a ∈ normGroup K L ↔ (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) a ∈ (GlobalNumberFields.ideleNormMap K L).range

The cyclic Hasse norm theorem. For a cyclic extension L/K of number fields, an element a ∈ Kˣ lies in N_{L/K}(Lˣ) exactly when its principal idele is the norm of an idele of L.

theorem TauCeti.ClassFieldTheory.isGlobalNorm_iff_isLocalNormEverywhere (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (a : Kˣ) : a ∈ normGroup K L ↔ GlobalNumberFields.IsLocalNormEverywhere K L a

The cyclic Hasse norm theorem, placewise. For a cyclic extension L/K of number fields, an element a ∈ Kˣ lies in N_{L/K}(Lˣ) exactly when, at every finite place v and every infinite place w of K, it is a norm from the local étale algebra K_v ⊗_K L, respectively K_w ⊗_K L.