The obstruction to lifting idele-class cohomology to the ideles

Let K be a number field and L/F a finite Galois layer inside Kˢ, cut out by open subgroups V ◁ U of G_K. The exact sequence 0 → (Kˢ)ˣ → I_{Kˢ} → C_{Kˢ} → 0 of discrete G_K-modules stays exact on V-invariants, because Hilbert 90 kills H¹(V, (Kˢ)ˣ): every idele class fixed by V is the class of an idele fixed by V (exists_ideleClassMk_eq_of_isClosed). On the layer this is the short exact sequence of Gal(L/F)-modules

0 → Lˣ → I_L → C_L → 0

(ideleShortComplex_shortExact). Its long exact cohomology sequence contains

H²(Gal(L/F), I_L) → H²(Gal(L/F), C_L) → H³(Gal(L/F), Lˣ),

whose first map is ideleToClassH2 and whose second, the connecting homomorphism, is classToMultiplicativeH3. The sum of local invariants is computed on H²(Gal(L/F), I_L) and descends only to the image of ideleToClassH2; range_ideleToClassH2 says that a class of H²(Gal(L/F), C_L) lies in that image exactly when its obstruction in H³(Gal(L/F), Lˣ) vanishes. Two lifts of one class differ by the image of H²(Gal(L/F), Lˣ) under the map multiplicativeToIdeleH2 induced by the principal ideles (ker_ideleToClassH2), and ideleToClassH2 commutes with inflation to a refinement of the layer (ideleToClassH2_cohomologyInfl).

The obstruction does not vanish in general: for the biquadratic field ℚ(√13, √17) every decomposition group has order at most two, so the image of H²(Gal, I_L) is killed by 2, while H²(Gal, C_L) is cyclic of order 4. For a cyclic layer it does vanish (surjective_ideleToClassH2_of_isCyclic), since there H³(Gal(L/F), Lˣ) ≅ H¹(Gal(L/F), Lˣ) by two-periodicity and the latter is zero by Hilbert 90.

Main definitions

• TauCeti.ClassFieldTheory.ideleShortExact K: the sequence 0 → (Kˢ)ˣ → I_{Kˢ} → C_{Kˢ} → 0 of discrete G_K-modules.
• TauCeti.ClassFieldTheory.principalIdeleHom K, TauCeti.ClassFieldTheory.ideleClassHom K: its two maps, between the coefficient modules of unitsFormation K, ideleFormation K and globalFormation K.
• TauCeti.ClassFieldTheory.ideleShortComplex K L: the sequence Lˣ → I_L → C_L of a layer.
• TauCeti.ClassFieldTheory.multiplicativeToIdeleH2 K L: the map H²(Gal(L/F), Lˣ) → H²(Gal(L/F), I_L).
• TauCeti.ClassFieldTheory.ideleToClassH2 K L: the map H²(Gal(L/F), I_L) → H²(Gal(L/F), C_L).
• TauCeti.ClassFieldTheory.classToMultiplicativeH3 K L: the connecting homomorphism H²(Gal(L/F), C_L) → H³(Gal(L/F), Lˣ).

Main statements

• TauCeti.ClassFieldTheory.exists_ideleClassMk_eq_of_isClosed: idele classes fixed by a closed subgroup of G_K are classes of ideles fixed by it.
• TauCeti.ClassFieldTheory.ideleShortComplex_shortExact: 0 → Lˣ → I_L → C_L → 0 is exact.
• TauCeti.ClassFieldTheory.ker_ideleToClassH2: the kernel of ideleToClassH2 is the image of multiplicativeToIdeleH2.
• TauCeti.ClassFieldTheory.range_ideleToClassH2: the image of ideleToClassH2 is the kernel of classToMultiplicativeH3.
• TauCeti.ClassFieldTheory.ideleToClassH2_cohomologyInfl: ideleToClassH2 commutes with inflation to a refinement of the layer.
• TauCeti.ClassFieldTheory.surjective_ideleToClassH2_of_isCyclic: on a cyclic layer every class of H²(Gal(L/F), C_L) lifts to H²(Gal(L/F), I_L).

Implementation notes

The formation of the multiplicative groups is unitsFormation K; its coefficient module is (Kˢ)ˣ, written additively as UnitsCoeff K, so Lˣ is its level at the top subgroup of the layer.

References

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

The exact sequence of ideles and idele classes

noncomputable def TauCeti.ClassFieldTheory.ideleShortExact (K : Type) [Field K] [NumberField K] : ContCohomology.DiscreteShortExact (AbsoluteGaloisGroup K) (UnitsCoeff K) (IdeleCoeff K) (IdeleClassCoeff K)

The sequence 0 → (Kˢ)ˣ → I_{Kˢ} → C_{Kˢ} → 0 of discrete G_K-modules, given by the principal ideles and the quotient map onto the idele classes.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleShortExact_incl (K : Type) [Field K] [NumberField K] : (ideleShortExact K).incl = ↑(principalIdele K)

The inclusion of ideleShortExact K is the embedding of the principal ideles.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleShortExact_proj (K : Type) [Field K] [NumberField K] : (ideleShortExact K).proj = ↑(ideleClassMk K)

The projection of ideleShortExact K is the quotient map onto the idele classes.

theorem TauCeti.ClassFieldTheory.exists_ideleClassMk_eq_of_isClosed {K : Type} [Field K] [NumberField K] (V : Subgroup (AbsoluteGaloisGroup K)) (hV : IsClosed ↑V) {c : IdeleClassCoeff K} (hc : ∀ v ∈ V, v • c = c) : ∃ (x : IdeleCoeff K), (∀ v ∈ V, v • x = x) ∧ (ideleClassMk K) x = c

Idele classes fixed by a closed subgroup lift to fixed ideles. If a closed subgroup V of G_K fixes an idele class c, then c is the class of an idele fixed by V. The obstruction is the connecting map H⁰(V, C_{Kˢ}) → H¹(V, (Kˢ)ˣ), whose target vanishes by Hilbert 90 for V. In field notation: the idele classes of the fixed field L of V are I_L / Lˣ.

The maps of formations

noncomputable def TauCeti.ClassFieldTheory.principalIdeleHom (K : Type) [Field K] [NumberField K] : (unitsFormation K).toRep ⟶ (ideleFormation K).toRep

The principal ideles as a map of formations: (Kˢ)ˣ → I_{Kˢ}, read on the coefficient modules of unitsFormation K and ideleFormation K.

@[simp]

theorem TauCeti.ClassFieldTheory.principalIdeleHom_hom_apply (K : Type) [Field K] [NumberField K] (x : UnitsCoeff K) : (Rep.Hom.hom (principalIdeleHom K)) ((unitsCoeffEquivUnitsFormation K) x) = (ideleCoeffEquivIdeleFormation K) ((principalIdele K) x)

principalIdeleHom K sends a unit of Kˢ to its principal idele.

noncomputable def TauCeti.ClassFieldTheory.ideleClassHom (K : Type) [Field K] [NumberField K] : (ideleFormation K).toRep ⟶ (globalFormation K).toRep

The quotient map onto the idele classes as a map of formations: I_{Kˢ} → C_{Kˢ}, read on the coefficient modules of ideleFormation K and globalFormation K.

@[simp]

theorem TauCeti.ClassFieldTheory.ideleClassHom_hom_apply (K : Type) [Field K] [NumberField K] (x : IdeleCoeff K) : (Rep.Hom.hom (ideleClassHom K)) ((ideleCoeffEquivIdeleFormation K) x) = (ideleClassCoeffEquivGlobalFormation K) ((ideleClassMk K) x)

ideleClassHom K sends an idele of Kˢ to its idele class.

The exact sequence 0 → Lˣ → I_L → C_L → 0 of a layer

theorem TauCeti.ClassFieldTheory.exact_principalIdeleHom_ideleClassHom (K : Type) [Field K] [NumberField K] : Function.Exact ⇑(Rep.Hom.hom (principalIdeleHom K)) ⇑(Rep.Hom.hom (ideleClassHom K))

The exactness of (Kˢ)ˣ → I_{Kˢ} → C_{Kˢ}, read on the coefficient modules of the three formations.

noncomputable def TauCeti.ClassFieldTheory.ideleShortComplex (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : CategoryTheory.ShortComplex (Rep ℤ L.Gal)

The sequence Lˣ → I_L → C_L of a layer: the coefficient modules of the units, idele and idele-class formations at the top of the layer, with the maps induced by the principal ideles and the quotient map onto the idele classes.

theorem TauCeti.ClassFieldTheory.ideleShortComplex_shortExact (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : (ideleShortComplex K L).ShortExact

The sequence 0 → Lˣ → I_L → C_L → 0 of a layer is exact. Exactness on the right is Hilbert 90 for the top subgroup of the layer, through exists_ideleClassMk_eq_of_isClosed.

The lifting obstruction

noncomputable def TauCeti.ClassFieldTheory.multiplicativeToIdeleH2 (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : ↑(L.H (unitsFormation K) 2) →+ ↑(L.H (ideleFormation K) 2)

The map H²(Gal(L/F), Lˣ) → H²(Gal(L/F), I_L) induced by the embedding Lˣ → I_L of the principal ideles of the layer.

theorem TauCeti.ClassFieldTheory.multiplicativeToIdeleH2_def (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : multiplicativeToIdeleH2 K L = (ModuleCat.Hom.hom ((groupCohomology.functor ℤ L.Gal 2).map (L.repMap (principalIdeleHom K)))).toAddMonoidHom

multiplicativeToIdeleH2 K L is the map induced in degree two by the principal ideles of the layer.

theorem TauCeti.ClassFieldTheory.multiplicativeToIdeleH2_apply (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (y : ↑(L.H (unitsFormation K) 2)) : (multiplicativeToIdeleH2 K L) y = (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap (principalIdeleHom K)) 2)) y

multiplicativeToIdeleH2 K L applies Mathlib's cohomology map of the principal ideles of the layer.

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

The comparison H²(Gal(L/F), I_L) → H²(Gal(L/F), C_L) induced by the quotient map I_L → C_L onto the idele classes of the layer.

theorem TauCeti.ClassFieldTheory.ideleToClassH2_def (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : ideleToClassH2 K L = (ModuleCat.Hom.hom ((groupCohomology.functor ℤ L.Gal 2).map (L.repMap (ideleClassHom K)))).toAddMonoidHom

ideleToClassH2 K L is the map induced in degree two by the quotient map onto the idele classes of the layer.

theorem TauCeti.ClassFieldTheory.ideleToClassH2_apply (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) (x : ↑(L.H (ideleFormation K) 2)) : (ideleToClassH2 K L) x = (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap (ideleClassHom K)) 2)) x

ideleToClassH2 K L applies Mathlib's cohomology map of the quotient map onto the idele classes of the layer.

noncomputable def TauCeti.ClassFieldTheory.classToMultiplicativeH3 (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : ↑(L.H (globalFormation K) 2) →+ ↑(L.H (unitsFormation K) 3)

The obstruction to lifting: the connecting homomorphism H²(Gal(L/F), C_L) → H³(Gal(L/F), Lˣ) of the exact sequence 0 → Lˣ → I_L → C_L → 0. Its target is the third cohomology of the layer in the multiplicative formation unitsFormation K.

theorem TauCeti.ClassFieldTheory.classToMultiplicativeH3_def (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : classToMultiplicativeH3 K L = (ModuleCat.Hom.hom (groupCohomology.δ ⋯ 2 3 ⋯)).toAddMonoidHom

classToMultiplicativeH3 K L is Mathlib's connecting homomorphism groupCohomology.δ of the exact sequence 0 → Lˣ → I_L → C_L → 0.

theorem TauCeti.ClassFieldTheory.ker_ideleToClassH2 (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : (ideleToClassH2 K L).ker = (multiplicativeToIdeleH2 K L).range

Exactness at the idele layer: a class of H²(Gal(L/F), I_L) vanishes in H²(Gal(L/F), C_L) exactly when it comes from H²(Gal(L/F), Lˣ).

theorem TauCeti.ClassFieldTheory.ideleToClassH2_cohomologyInfl (K : Type) [Field K] [NumberField K] {old new : NormalLayer (AbsoluteGaloisGroup K)} (T : LayerRefinement old new) (x : ↑(old.H (ideleFormation K) 2)) : (ideleToClassH2 K new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (ideleFormation K) 2)) x) = (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl (globalFormation K) 2)) ((ideleToClassH2 K old) x)

The comparison with idele classes commutes with inflation: for a refinement L'/F of the layer L/F, mapping the inflation of a class of H²(Gal(L/F), I_L) to H²(Gal(L'/F), C_{L'}) is inflating its image in H²(Gal(L/F), C_L).

theorem TauCeti.ClassFieldTheory.range_ideleToClassH2 (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) : (ideleToClassH2 K L).range = (classToMultiplicativeH3 K L).ker

Exactness at the idele-class layer: a class of H²(Gal(L/F), C_L) lifts to H²(Gal(L/F), I_L) exactly when its obstruction in H³(Gal(L/F), Lˣ) vanishes.

theorem TauCeti.ClassFieldTheory.surjective_ideleToClassH2_of_isCyclic (K : Type) [Field K] [NumberField K] (L : NormalLayer (AbsoluteGaloisGroup K)) [IsCyclic L.Gal] : Function.Surjective ⇑(ideleToClassH2 K L)

On a cyclic layer every class of H²(Gal(L/F), C_L) lifts to the ideles. For cyclic Gal(L/F), H³(Gal(L/F), Lˣ) ≅ H¹(Gal(L/F), Lˣ) by two-periodicity, and the latter vanishes by Hilbert 90, so the obstruction classToMultiplicativeH3 is zero.