The Tate cohomology of the finite S-ideles

Let L/K be a cyclic extension of number fields and S a finite set of finite places of K containing every place ramified in L. The finite S-ideles of L are, as a representation of Gal(L/K), the product of the semi-local factors ∏_{w ∣ v} L_wˣ for v ∈ S and ∏_{w ∣ v} 𝒪_wˣ for v ∉ S (TauCeti.finiteSIdelesPiIso). The factors of the second kind have no Tate cohomology, because v is unramified. Since Tate cohomology commutes with products (TauCeti.TateCohomology.linearEquivPi), the Tate cohomology of the finite S-ideles is, in every degree,

H-hat^n(Gal(L/K), I_{L,S}^f) ≃ ∏_{v ∈ S} H-hat^n(Gal(L/K), (K_v ⊗[K] L)ˣ),

and by Shapiro's lemma each factor is H-hat^n(Gal(L_w/K_v), L_wˣ) for a place w above v (semilocalUnitsTateCohomologyIso). In degree 2 this is the finite part of the description of H²(Gal(L/K), I_L) by the local Brauer groups Br(L_w/K_v) (Milne, Class Field Theory, VII, Proposition 2.5), through which the local invariants of an idele class are read.

A factor of the first kind has Herbrand quotient the local degree [L_w : K_v], and the Herbrand quotient of a product is the product of the Herbrand quotients of the factors outside a cohomologically trivial part (TauCeti.TateCohomology.herbrandQuotient_pi), so

h(I_{L,S}^f) = ∏_{v ∈ S} [L_w : K_v].

Together with the factors at the infinite places, this is the Herbrand quotient of the S-ideles I_{L,S}, the idelic half of the computation h(C_L) = [L : K] of the Herbrand quotient of the idele classes, from which the first fundamental inequality for cyclic extensions follows.

Main definitions

• TauCeti.ClassFieldTheory.placeAbove: a choice of a place of L above each place of S.
• TauCeti.ClassFieldTheory.finiteSIdelesTateCohomologyEquiv: for L/K cyclic and unramified outside S, H-hat^n(Gal(L/K), I_{L,S}^f) ≃ ∏_{v ∈ S} H-hat^n(Gal(L/K), (K_v ⊗[K] L)ˣ).

Main results

• TauCeti.ClassFieldTheory.finiteSIdelesTateCohomologyEquiv_apply: its component at v ∈ S is induced by the semi-local component at v.
• TauCeti.ClassFieldTheory.herbrandQuotient_finiteSIdelesRep: for L/K cyclic and unramified outside S, h(I_{L,S}^f) = ∏_{v ∈ S} [L_w : K_v], for any choice of places w above the places of S.
• TauCeti.ClassFieldTheory.finite_tateCohomology_finiteSIdelesRep: the Tate cohomology of the finite S-ideles is finite in degrees 0 and -1.

References

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

noncomputable def TauCeti.ClassFieldTheory.placeAbove {K : Type} [Field K] (L : Type) [Field L] [Algebra K L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (v : ↥S) : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver (↑v).asIdeal }

A choice of a place of L above each place of a finite set S of finite places of K.

noncomputable def TauCeti.ClassFieldTheory.finiteSIdelesTateCohomologyEquiv {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w ∉ S → Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal) (n : ℤ) : ↑(tateCohomology (finiteSIdelesRep L S) n) ≃+ ((v : ↥S) → ↑(tateCohomology (semilocalUnitsRep L ↑v) n))

The Tate cohomology of the finite S-ideles is the product of the semi-local Tate cohomologies at the places of S. For a cyclic extension L/K of number fields and a finite set S of finite places of K outside which L/K is unramified,

H-hat^n(Gal(L/K), I_{L,S}^f) ≃ ∏_{v ∈ S} H-hat^n(Gal(L/K), (K_v ⊗[K] L)ˣ)

in every degree n : ℤ, the component at v being induced by the semi-local component at v (finiteSIdelesTateCohomologyEquiv_apply). The factors at the places outside S drop out, having no Tate cohomology. By Shapiro's lemma (semilocalUnitsTateCohomologyIso) each factor is the Tate cohomology H-hat^n(Gal(L_w/K_v), L_wˣ) of the completion at a place w above v.

@[simp]

theorem TauCeti.ClassFieldTheory.finiteSIdelesTateCohomologyEquiv_apply {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w ∉ S → Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal) (n : ℤ) (x : ↑(tateCohomology (finiteSIdelesRep L S) n)) (v : ↥S) : (finiteSIdelesTateCohomologyEquiv S hS n) x v = (ModuleCat.Hom.hom ((tateCohomologyFunctor n).map (CategoryTheory.CategoryStruct.comp (finiteSIdelesPiIso L S).hom (Rep.piProj (Sum.elim (fun (v : ↥S) => semilocalUnitsRep L ↑v) fun (v : { v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) // v ∉ S }) => semilocalIntegralUnitsRep L ↑v) (Sum.inl v))))) x

The component at v ∈ S of finiteSIdelesTateCohomologyEquiv is induced by the semi-local component at v, the factor at v of finiteSIdelesPiIso.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_finiteSIdelesRep {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w ∉ S → Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal) (w : (v : ↥S) → { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver (↑v).asIdeal }) : TateCohomology.herbrandQuotient (finiteSIdelesRep L S) = ∏ v : ↥S, ↑(Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑(w v)))

The Herbrand quotient of the finite S-ideles. For a cyclic extension L/K of number fields and a finite set S of finite places of K outside which L/K is unramified, the finite S-ideles of L have Herbrand quotient ∏_{v ∈ S} [L_w : K_v] as a representation of Gal(L/K), for any choice of a place w of L above each v ∈ S.

theorem TauCeti.ClassFieldTheory.herbrandQuotient_finiteSIdelesRep_ne_zero {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w ∉ S → Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal) : TateCohomology.herbrandQuotient (finiteSIdelesRep L S) ≠ 0

For a cyclic extension L/K of number fields unramified outside a finite set S of finite places of K, the Herbrand quotient of the finite S-ideles is nonzero: by herbrandQuotient_finiteSIdelesRep it is a product of local degrees.

theorem TauCeti.ClassFieldTheory.finite_tateCohomology_finiteSIdelesRep {K : Type} [Field K] [NumberField K] {L : Type} [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hS : ∀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w ∉ S → Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal) : Finite ↑(tateCohomology (finiteSIdelesRep L S) 0) ∧ Finite ↑(tateCohomology (finiteSIdelesRep L S) (-1))

The Tate cohomology of the finite S-ideles is finite in degrees 0 and -1, for a cyclic extension L/K of number fields unramified outside a finite set S of finite places of K.