The second fundamental inequality

Let K be a number field. The second fundamental inequality for the idele-class formation globalFormation K says that #H²(U/V, C_L) ∣ [U : V] on every finite normal layer V ◁ U, and it comes together with the vanishing of H¹(U/V, C_L) (Milne, Class Field Theory, VII, Theorem 5.1). Classically both are reduced, by Sylow and tower arguments, to cyclic extensions of prime degree p, and then, by adjoining the p-th roots of unity, to the Kummer case: for a cyclic extension L/F of number fields of prime degree p whose ground field F contains the p-th roots of unity,

[C_F : N_{L/F}(C_L)] ≤ p.

This file assembles that reduction for the idele-class formation. The Kummer index computation (index_range_ideleClassNormMap_le_of_finrank_prime) shows that the Kummer case holds for all number fields. It therefore gives H¹ = 0 and #H² ∣ [U : V] for every layer of globalFormation K (subsingleton_h1_globalFormation, natCard_H2_globalFormation_dvd_degree).

The steps are the following.

• A layer V ◁ U whose ground field F, the fixed field of U, contains the p-th roots of unity of Kˢ and whose degree is p is read on number fields: with L the fixed field of V, the extension L/F is Galois of degree p (NormalLayer.galEquivOfFixedField), F contains a primitive p-th root of unity, and the norm quotient of the layer is C_F / N_{L/F}(C_L) (NormalLayer.ideleClassNormQuotientEquiv). The Kummer case bounds its order by p.
• With the first inequality (degree_le_natCard_normQuotient_of_isCyclic), the norm quotient of every such layer has exactly p elements, and adjoining the p-th roots of unity, a step of degree prime to p, carries the divisibility #(C_F / N_{L/F}(C_L)) ∣ p to every layer of prime degree p (NormalLayer.natCard_normQuotient_dvd_prime_of_adjoin_nth_roots). So every layer of prime degree has norm quotient of order its degree (natCard_normQuotient_globalFormation_eq_degree_of_prime).
• A layer of prime degree is cyclic, so its Herbrand quotient is its degree (herbrandQuotient_rep_globalFormation_eq_degree). The reduction to layers of prime degree (NormalLayer.subsingleton_h1_of_herbrandQuotient_of_prime_degree, NormalLayer.natCard_H2_dvd_degree_of_herbrandQuotient_of_prime_degree) then gives the two statements for every layer.

Main results

• TauCeti.ClassFieldTheory.natCard_normQuotient_globalFormation_eq_degree_of_prime: a layer of prime degree has norm quotient of order its degree.
• TauCeti.ClassFieldTheory.subsingleton_h1_globalFormation: H¹ of every layer of the idele-class formation vanishes.
• TauCeti.ClassFieldTheory.subsingleton_groupCohomology_one_ideleClassRep: H¹(Gal(L/K), C_L) vanishes for every finite Galois extension L/K of number fields.
• TauCeti.ClassFieldTheory.natCard_H2_globalFormation_dvd_degree: the second fundamental inequality for every layer of the idele-class formation.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §5 (Theorem 5.1 and its reduction to the Kummer case) and §6.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §4.

theorem TauCeti.ClassFieldTheory.natCard_normQuotient_globalFormation_eq_degree_of_prime {K : Type} [Field K] [NumberField K] (Lay : NormalLayer (AbsoluteGaloisGroup K)) (hp : Nat.Prime Lay.degree) : Nat.card (Lay.NormQuotient (globalFormation K)) = Lay.degree

The norm quotient on a layer of prime degree has order its degree.

theorem TauCeti.ClassFieldTheory.subsingleton_h1_globalFormation {K : Type} [Field K] [NumberField K] (Lay : NormalLayer (AbsoluteGaloisGroup K)) : Subsingleton ↑(Lay.H (globalFormation K) 1)

H¹ of the global idele-class formation vanishes. For every finite normal layer V ◁ U of G_K, the group H¹(U/V, C_L) is trivial.

theorem TauCeti.ClassFieldTheory.subsingleton_groupCohomology_one_ideleClassRep (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : Subsingleton ↑(groupCohomology (ideleClassRep K L) 1)

H¹ of the idele classes of a finite Galois extension vanishes. For every finite Galois extension L/K of number fields, H¹(Gal(L/K), C_L) is trivial.

theorem TauCeti.ClassFieldTheory.natCard_H2_globalFormation_dvd_degree {K : Type} [Field K] [NumberField K] (Lay : NormalLayer (AbsoluteGaloisGroup K)) : Nat.card ↑(Lay.H (globalFormation K) 2) ∣ Lay.degree

The second fundamental inequality for the global idele-class formation. For every finite normal layer V ◁ U of G_K, the order of H²(U/V, C_L) divides [U : V].