The global invariant and the idele-class formation

Let K be a number field. Tate's construction of the invariant map of the idele classes defines, on a finite normal layer L/F inside Kˢ, the invariant of a class of H²(Gal(L/F), C_L) as the sum of the local invariants ideleSumLocalInv of a lift of its inflation to the ideles of some refinement of the layer. This file carries out that construction for the idele-class formation globalFormation K and shows that it makes globalFormation K a class formation.

From the sum formula for the Brauer group of K (sumLocalInv_brLocalization_eq_zero), the sum of the local invariants vanishes on the kernel of H²(Gal(L/F), I_L) → H²(Gal(L/F), C_L) and does not depend on the choice of lift and refinement. Every layer of prime degree p carries a class of H²(Gal(L/F), I_L) whose local invariants sum to 1/p (exists_ideleSumLocalInv_eq_one_div_degree_of_prime); its image generates H²(Gal(L/F), C_L), whose order divides p by the second inequality. The reduction to layers of prime degree then shows that the kernel above is exactly the set of classes whose local invariants sum to zero, and that every class of H²(Gal(L/F), C_L) lifts to the ideles after inflation to a suitable refinement.

These are the hypotheses of descendedInv and ClassFormation.ofDescendedInv: the global invariant globalInv K L is the invariant descended from ideleSumLocalInv, and the global class formation is the class formation it defines. The idele-class H¹ vanishes by the first and second inequalities (subsingleton_h1_globalFormation), and the cyclotomic input exists_refinement_ideleSumLocalInv_eq supplies a class of invariant 1/[L:F] on a refinement of every layer, which makes the invariant of a layer of degree n an isomorphism onto the n-torsion of ℚ/ℤ.

Main definitions

• TauCeti.ClassFieldTheory.globalInv: the invariant H²(Gal(L/F), C_L) → ℚ/ℤ of a layer.
• TauCeti.ClassFieldTheory.globalClassFormation: the idele-class formation of K as a class formation, with invariant globalInv (globalClassFormation_inv).

Main statements

All in the namespace TauCeti.ClassFieldTheory:

• ideleToClassH2_eq_zero_iff: a class of H²(Gal(L/F), I_L) dies in the idele classes exactly when its local invariants sum to zero.
• exists_refinement_mem_range_ideleToClassH2: after inflation to a refinement, every class of H²(Gal(L/F), C_L) lifts to the ideles.
• ideleSumLocalInv_eq_of_ideleToClassH2_eq: two lifts of the inflations of one class to two refinements have the same sum of local invariants.
• globalInv_eq: the global invariant of a class is the sum of the local invariants of any lift of any of its inflations.
• globalInv_ideleToClassH2, globalInv_infl and globalInv_unique: the two equations that determine the global invariant.
• globalInv_res, globalInv_conj: its restriction and conjugation laws.
• globalInv_injective, range_globalInv: the global invariant of a layer of degree n is injective with image the n-torsion of ℚ/ℤ.
• ideleSumLocalInv_fundamentalClass: the local invariants of any idele lift of the fundamental class of the global class formation sum to 1/[L:F].

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §§5–8, and Chapter VIII, §4 (Theorem 4.7).
• J. Tate, Global class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VII, §11.

Consequences of the sum formula

theorem TauCeti.ClassFieldTheory.ideleSumLocalInv_eq_zero_of_ideleToClassH2_eq_zero {K : Type} [Field K] [NumberField K] {L : NormalLayer (AbsoluteGaloisGroup K)} {y : ↑(L.H (ideleFormation K) 2)} (hy : (ideleToClassH2 K L) y = 0) : (ideleSumLocalInv K L) y = 0

The sum of the local invariants vanishes on the classes that die in the idele classes.

theorem TauCeti.ClassFieldTheory.ideleSumLocalInv_eq_of_ideleToClassH2_eq {K : Type} [Field K] [NumberField K] {Lay Lay₁ Lay₂ : NormalLayer (AbsoluteGaloisGroup K)} (T₁ : LayerRefinement Lay Lay₁) (T₂ : LayerRefinement Lay Lay₂) (x : ↑(Lay.H (globalFormation K) 2)) (y₁ : ↑(Lay₁.H (ideleFormation K) 2)) (y₂ : ↑(Lay₂.H (ideleFormation K) 2)) (h₁ : (ideleToClassH2 K Lay₁) y₁ = (CategoryTheory.ConcreteCategory.hom (T₁.cohomologyInfl (globalFormation K) 2)) x) (h₂ : (ideleToClassH2 K Lay₂) y₂ = (CategoryTheory.ConcreteCategory.hom (T₂.cohomologyInfl (globalFormation K) 2)) x) : (ideleSumLocalInv K Lay₁) y₁ = (ideleSumLocalInv K Lay₂) y₂

Independence of the lift and of the refinement: two lifts to the ideles of the inflations of one class of H²(Gal(L/F), C_L), to two refinements of the layer, have the same sum of local invariants.

The kernel of the passage to idele classes

theorem TauCeti.ClassFieldTheory.ideleToClassH2_eq_zero_iff {K : Type} [Field K] [NumberField K] {L : NormalLayer (AbsoluteGaloisGroup K)} {y : ↑(L.H (ideleFormation K) 2)} : (ideleToClassH2 K L) y = 0 ↔ (ideleSumLocalInv K L) y = 0

A class of the idele layer dies in the idele classes exactly when its local invariants sum to zero.

theorem TauCeti.ClassFieldTheory.exists_refinement_mem_range_ideleToClassH2 {K : Type} [Field K] [NumberField K] (Lay : NormalLayer (AbsoluteGaloisGroup K)) : ∃ (Lay' : NormalLayer (AbsoluteGaloisGroup K)) (T : LayerRefinement Lay Lay'), ∀ (x : ↑(Lay.H (globalFormation K) 2)), (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (globalFormation K) 2)) x ∈ (ideleToClassH2 K Lay').range

Killing the obstruction: some refinement of every layer L/F is such that the inflation of every class of H²(Gal(L/F), C_L) to it lifts to the ideles.

The global invariant

noncomputable def TauCeti.ClassFieldTheory.globalInv (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : ↑(L.H (globalFormation K) 2) →+ AddCircle 1

The global invariant H²(Gal(L/F), C_L) → ℚ/ℤ of a finite normal layer L/F inside Kˢ: the invariant of a class is the sum of the local invariants of a lift to the ideles of its inflation to some refinement of the layer. By globalInv_eq it does not depend on the refinement or on the lift, and globalInv_unique characterizes it by the equations globalInv_ideleToClassH2 and globalInv_infl.

theorem TauCeti.ClassFieldTheory.globalInv_eq {K : Type} [Field K] [NumberField K] {L L' : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement L L') {x : ↑(L.H (globalFormation K) 2)} {y : ↑(L'.H (ideleFormation K) 2)} (h : (ideleToClassH2 K L') y = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (globalFormation K) 2)) x) : (globalInv K L) x = (ideleSumLocalInv K L') y

The global invariant of a class is the sum of the local invariants of a lift of an inflation of it: if the inflation of x to a refinement L' of L is the idele class of y, then globalInv K L x is the sum of the local invariants of y.

@[simp]

theorem TauCeti.ClassFieldTheory.globalInv_ideleToClassH2 {K : Type} [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (y : ↑(L.H (ideleFormation K) 2)) : (globalInv K L) ((ideleToClassH2 K L) y) = (ideleSumLocalInv K L) y

The sum formula, the first defining equation of the global invariant: the invariant of the idele class of a class of H²(Gal(L/F), I_L) is the sum of its local invariants.

@[simp]

theorem TauCeti.ClassFieldTheory.globalInv_infl {K : Type} [Field K] [NumberField K] {L L' : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement L L') (x : ↑(L.H (globalFormation K) 2)) : (globalInv K L') ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (globalFormation K) 2)) x) = (globalInv K L) x

Inflation invariance, the second defining equation of the global invariant.

theorem TauCeti.ClassFieldTheory.globalInv_unique {K : Type} [Field K] [NumberField K] (f : (L : NormalLayer (AbsoluteGaloisGroup K)) → ↑(L.H (globalFormation K) 2) →+ AddCircle 1) (hdesc : ∀ (L : NormalLayer (AbsoluteGaloisGroup K)) (y : ↑(L.H (ideleFormation K) 2)), (f L) ((ideleToClassH2 K L) y) = (ideleSumLocalInv K L) y) (hinfl : ∀ {L L' : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement L L') (x : ↑(L.H (globalFormation K) 2)), (f L') ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (globalFormation K) 2)) x) = (f L) x) : f = globalInv K

The global invariant is determined by its two equations: a family of homomorphisms H²(Gal(L/F), C_L) → ℚ/ℤ that is the sum of the local invariants on idele classes and does not change under inflation is the global invariant.

@[simp]

theorem TauCeti.ClassFieldTheory.globalInv_res {K : Type} [Field K] [NumberField K] {small big : NormalLayer (AbsoluteGaloisGroup K)} (R : LayerRestriction small big) (x : ↑(big.H (globalFormation K) 2)) : (globalInv K small) ((CategoryTheory.ConcreteCategory.hom (R.cohomologyRes (globalFormation K) 2)) x) = R.relativeDegree • (globalInv K big) x

Restriction multiplies the global invariant by the relative degree.

@[simp]

theorem TauCeti.ClassFieldTheory.globalInv_conj {K : Type} [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (g : AbsoluteGaloisGroup K) (x : ↑(L.H (globalFormation K) 2)) : (globalInv K (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso (globalFormation K) g 2).hom) x) = (globalInv K L) x

Conjugation preserves the global invariant.

theorem TauCeti.ClassFieldTheory.globalInv_injective {K : Type} [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : Function.Injective ⇑(globalInv K L)

The global invariant is injective, because the idele-class H¹ vanishes and the sum of the local invariants vanishes only on the classes that die in the idele classes.

theorem TauCeti.ClassFieldTheory.range_globalInv {K : Type} [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : Set.range ⇑(globalInv K L) = ↑(AddSubgroup.torsionBy (AddCircle 1) ↑L.degree)

The image of the global invariant of a layer of degree n is the n-torsion of ℚ/ℤ.

The global class formation

noncomputable def TauCeti.ClassFieldTheory.globalClassFormation (K : Type) [Field K] [NumberField K] : ClassFormation (globalFormation K)

The global class formation: the idele-class formation of K is a class formation, whose invariant on a layer is the global invariant (globalClassFormation_inv).

@[simp]

theorem TauCeti.ClassFieldTheory.globalClassFormation_inv {K : Type} [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : (globalClassFormation K).inv L = globalInv K L

The invariant of the global class formation is the global invariant, the sum of the local invariants of a lift to the ideles.

theorem TauCeti.ClassFieldTheory.ideleSumLocalInv_fundamentalClass {K : Type} [Field K] [NumberField K] {L : NormalLayer (AbsoluteGaloisGroup K)} {y : ↑(L.H (ideleFormation K) 2)} (hy : (ideleToClassH2 K L) y = (globalClassFormation K).fundamentalClass L) : (ideleSumLocalInv K L) y = ↑(1 / ↑L.degree)

The local invariants of an idele lift of the fundamental class sum to 1/[L:F]: if the idele class of y is the fundamental class of the layer L/F in the global class formation, then the local invariants of y sum to 1/[L:F].