The cohomology of the ideles, place by place

Let L/K be a finite Galois extension of number fields with Galois group G. The ideles I_L of L, as a representation of G, map to the semi-local unit groups (K_v ⊗[K] L)ˣ ≃ ∏_{w ∣ v} L_wˣ at every place v of K, finite (idelesToSemilocalUnits) or infinite (idelesToInfiniteSemilocalUnits). This file shows that in every positive degree n these maps identify the cohomology of the ideles with the direct sum of the semi-local cohomology groups,

H^n(G, I_L) ≃ ⨁_v H^n(G, (K_v ⊗[K] L)ˣ)

(idelesCohomologyLocalizationEquiv), the sum running over the finite and the infinite places:

• a class of H^n(G, I_L) whose images in all the groups H^n(G, (K_v ⊗[K] L)ˣ) vanish is zero (eq_zero_of_forall_map_semilocal_eq_zero);
• only finitely many of its images at the finite places are nonzero (finite_setOf_map_idelesToSemilocalUnits_ne_zero);
• every finitely supported family of semi-local classes is the family of images of a class (idelesCohomologyLocalization_surjective);
• its first cohomology vanishes (isZero_tateCohomology_one_idelesRep), by field Hilbert 90 and Shapiro at every finite and infinite place, without a cyclicity hypothesis.

By positive-degree Shapiro (HeightOneSpectrum.semilocalUnitsTateCohomologyIsoPos at the finite places, InfinitePlace.infiniteSemilocalUnitsTateCohomologyIsoPos at the infinite places) the group H^n(G, (K_v ⊗[K] L)ˣ) is the cohomology H^n(G_w, L_wˣ) of the completion at a place w ∣ v, so the images of a degree-2 cohomology class with coefficients in the ideles are its local Brauer classes in Br(L_w/K_v), and H²(G, I_L) is the direct sum of the local Brauer groups Br(L_w/K_v). The first statement is the idelic half of the injectivity of Br(L/K) → ⨁_v Br(L_w/K_v); the other half is the vanishing of H¹(G, C_L).

The proof is Milne's (Class Field Theory, VII, Lemma 2.4 and Proposition 2.5). The ideles are the union of the S-ideles over the finite sets S of finite places, so every class comes from the S-ideles for a finite S that may be taken to contain the places ramified in L (TauCeti.TateCohomology.exists_tateCohomologyFunctor_map_eq). The S-ideles split as I_{L,S} = L_∞ˣ × I_{L,S}^f (sIdeles_hom_decomp), the infinite ideles are the product of the archimedean semi-local unit groups (TauCeti.GlobalNumberFields.infiniteIdelesPiIso), and the finite S-ideles are the product of the semi-local unit groups at S and of the integral semi-local unit groups away from S (TauCeti.finiteSIdelesPiIso). Tate cohomology commutes with products (TauCeti.TateCohomology.linearEquivPi), and the integral factors, at places unramified in L, have no cohomology in positive degrees (isZero_tateCohomology_semilocalIntegralUnitsRep_of_neZero). Read backwards, the same decomposition prescribes the semi-local components: a family supported on such an S is the image of a class of the S-ideles, built factor by factor.

Main definitions

• TauCeti.ClassFieldTheory.idelesToSemilocalUnits L v, TauCeti.ClassFieldTheory.idelesToInfiniteSemilocalUnits L w: the semi-local components of an idele at a finite place v and at an infinite place w of K.
• TauCeti.ClassFieldTheory.idelesCohomologyLocalization K L n: the map H^n(G, I_L) → ⨁_v H^n(G, (K_v ⊗[K] L)ˣ) taking a class to its semi-local components.
• TauCeti.ClassFieldTheory.idelesCohomologyLocalizationEquiv K L n: the same map, as an isomorphism for n > 0.

Main results

• TauCeti.ClassFieldTheory.eq_zero_of_forall_map_semilocal_eq_zero: a class of H^n(G, I_L), n > 0, with vanishing semi-local components is zero.
• TauCeti.ClassFieldTheory.finite_setOf_map_idelesToSemilocalUnits_ne_zero: a class of H^n(G, I_L), n > 0, has nonzero semi-local components at only finitely many finite places.
• TauCeti.ClassFieldTheory.idelesCohomologyLocalization_surjective: for n > 0, every finitely supported family of semi-local classes is the family of semi-local components of a class.
• TauCeti.ClassFieldTheory.isZero_tateCohomology_one_idelesRep: Hilbert 90 for ideles, on the Tate carrier.
• TauCeti.ClassFieldTheory.subsingleton_groupCohomology_one_idelesRep: Hilbert 90 on ordinary cohomology, as an instance.

In the long exact cohomology sequence of Lˣ → I_L → C_L, idelic Hilbert 90 makes H¹(Gal(L/K), C_L) → H²(Gal(L/K), Lˣ) injective. Thus vanishing of idele-class H¹ is equivalent to injectivity of the map from relative Brauer classes to idelic cohomology.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Lemma 2.4, Proposition 2.5 and Corollary 2.6.
• J. Tate, Global class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VII, §§6–7.

The semi-local components of an idele

noncomputable def TauCeti.ClassFieldTheory.idelesToSemilocalUnits {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : idelesRep K L ⟶ semilocalUnitsRep L v

The semi-local component of an idele at a finite place v of K, its components at the places w ∣ v of L as a unit of K_v ⊗[K] L ≃ ∏_{w ∣ v} L_w, as a morphism of representations of Aut(L/K).

@[simp]

theorem TauCeti.ClassFieldTheory.idelesToSemilocalUnits_hom_apply {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : Additive (NumberField.IdeleGroup (NumberField.RingOfIntegers L) L)) : (Rep.Hom.hom (idelesToSemilocalUnits L v)) x = Additive.ofMul ((finiteIdeleSemilocalHom L v) ((NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers L) L) (Additive.toMul x)))

idelesToSemilocalUnits L v is the semi-local component at v of the finite part.

noncomputable def TauCeti.ClassFieldTheory.idelesToInfiniteSemilocalUnits {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] (w : NumberField.InfinitePlace K) : idelesRep K L ⟶ GlobalNumberFields.infiniteSemilocalUnitsRep L w

The semi-local component of an idele at an infinite place w of K, its components at the places of L above w as a unit of K_w ⊗[K] L, as a morphism of representations of Aut(L/K).

@[simp]

theorem TauCeti.ClassFieldTheory.coe_idelesToInfiniteSemilocalUnits_hom_apply {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] (w : NumberField.InfinitePlace K) (x : Additive (NumberField.IdeleGroup (NumberField.RingOfIntegers L) L)) : ↑(Additive.toMul ((Rep.Hom.hom (idelesToInfiniteSemilocalUnits L w)) x)) = (GlobalNumberFields.infiniteAdeleSemilocalHom L w) (↑(Additive.toMul x)).1

idelesToInfiniteSemilocalUnits L w is the semi-local component at w of the infinite part.

The S-ideles inside the ideles

The cohomology of the ideles

theorem TauCeti.ClassFieldTheory.eq_zero_of_forall_map_semilocal_eq_zero {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) [NeZero n] {x : ↑(tateCohomology (idelesRep K L) ↑n)} (hfin : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (ModuleCat.Hom.hom ((tateCohomologyFunctor ↑n).map (idelesToSemilocalUnits L v))) x = 0) (hinf : ∀ (w : NumberField.InfinitePlace K), (ModuleCat.Hom.hom ((tateCohomologyFunctor ↑n).map (idelesToInfiniteSemilocalUnits L w))) x = 0) : x = 0

The cohomology of the ideles is detected place by place. For a finite Galois extension L/K of number fields and n > 0, a class of H^n(Gal(L/K), I_L) whose images in H^n(Gal(L/K), (K_v ⊗[K] L)ˣ) vanish at every finite and every infinite place v of K is zero.

theorem TauCeti.ClassFieldTheory.finite_setOf_map_idelesToSemilocalUnits_ne_zero {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) [NeZero n] (x : ↑(tateCohomology (idelesRep K L) ↑n)) : {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) | (ModuleCat.Hom.hom ((tateCohomologyFunctor ↑n).map (idelesToSemilocalUnits L v))) x ≠ 0}.Finite

The semi-local components of a cohomology class with coefficients in the ideles are finitely supported. For a finite Galois extension L/K of number fields and n > 0, a class of H^n(Gal(L/K), I_L) has nonzero image in H^n(Gal(L/K), (K_v ⊗[K] L)ˣ) at only finitely many finite places v of K.

Prescribing the semi-local components

noncomputable def TauCeti.ClassFieldTheory.idelesCohomologyLocalization (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) [NeZero n] : ↑(tateCohomology (idelesRep K L) ↑n) →+ (Π₀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑(tateCohomology (semilocalUnitsRep L v) ↑n)) × ((w : NumberField.InfinitePlace K) → ↑(tateCohomology (GlobalNumberFields.infiniteSemilocalUnitsRep L w) ↑n))

The semi-local components of the cohomology of the ideles. For a finite Galois extension L/K of number fields and n > 0, the map H^n(Gal(L/K), I_L) → ⨁_v H^n(Gal(L/K), (K_v ⊗[K] L)ˣ) taking a class to its semi-local components, as a finitely supported family at the finite places (finite_setOf_map_idelesToSemilocalUnits_ne_zero) together with a family at the infinite places. It is an isomorphism (idelesCohomologyLocalizationEquiv).

@[simp]

theorem TauCeti.ClassFieldTheory.idelesCohomologyLocalization_fst_apply {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) [NeZero n] (x : ↑(tateCohomology (idelesRep K L) ↑n)) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : ((idelesCohomologyLocalization K L n) x).1 v = (ModuleCat.Hom.hom ((tateCohomologyFunctor ↑n).map (idelesToSemilocalUnits L v))) x

The component of idelesCohomologyLocalization at a finite place v is induced by the semi-local component at v.

@[simp]

theorem TauCeti.ClassFieldTheory.idelesCohomologyLocalization_snd_apply {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) [NeZero n] (x : ↑(tateCohomology (idelesRep K L) ↑n)) (w : NumberField.InfinitePlace K) : ((idelesCohomologyLocalization K L n) x).2 w = (ModuleCat.Hom.hom ((tateCohomologyFunctor ↑n).map (idelesToInfiniteSemilocalUnits L w))) x

The component of idelesCohomologyLocalization at an infinite place w is induced by the semi-local component at w.

theorem TauCeti.ClassFieldTheory.idelesCohomologyLocalization_injective (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) [NeZero n] : Function.Injective ⇑(idelesCohomologyLocalization K L n)

A class with coefficients in the ideles is determined by its semi-local components.

theorem TauCeti.ClassFieldTheory.idelesCohomologyLocalization_surjective (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) [NeZero n] : Function.Surjective ⇑(idelesCohomologyLocalization K L n)

Every finitely supported family of semi-local classes is the family of semi-local components of a class with coefficients in the ideles.

noncomputable def TauCeti.ClassFieldTheory.idelesCohomologyLocalizationEquiv (K : Type) [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) [NeZero n] : ↑(tateCohomology (idelesRep K L) ↑n) ≃+ (Π₀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑(tateCohomology (semilocalUnitsRep L v) ↑n)) × ((w : NumberField.InfinitePlace K) → ↑(tateCohomology (GlobalNumberFields.infiniteSemilocalUnitsRep L w) ↑n))

The cohomology of the ideles is the direct sum of the semi-local cohomology groups. For a finite Galois extension L/K of number fields and n > 0, H^n(Gal(L/K), I_L) ≃ ⨁_v H^n(Gal(L/K), (K_v ⊗[K] L)ˣ), the sum running over the finite and the infinite places of K, by taking semi-local components.

@[simp]

theorem TauCeti.ClassFieldTheory.coe_idelesCohomologyLocalizationEquiv {K : Type} [Field K] [NumberField K] (L : Type) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) [NeZero n] : ⇑(idelesCohomologyLocalizationEquiv K L n) = ⇑(idelesCohomologyLocalization K L n)

idelesCohomologyLocalizationEquiv takes a class to its semi-local components.

theorem TauCeti.ClassFieldTheory.isZero_tateCohomology_one_idelesRep {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : CategoryTheory.Limits.IsZero (tateCohomology (idelesRep K L) 1)

Hilbert 90 for ideles. The first Tate cohomology of the idele module of a finite Galois extension of number fields vanishes.

instance TauCeti.ClassFieldTheory.subsingleton_groupCohomology_one_idelesRep {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : Subsingleton ↑(groupCohomology (idelesRep K L) 1)

Hilbert 90 for ideles, on ordinary group cohomology: H¹(Gal(L/K), I_L) = 0.