Tate cohomology of S-units

For a finite set S of finite places of a number field K and an extension of number fields L/K, the S-units U_{L,S} of L are finitely generated. Consequently their degree-zero and degree-minus-one Tate cohomology groups are finite. These are the finiteness inputs in the short exact sequence U_{L,S} → I_{L,S} → C_L used to compute the Herbrand quotient of idele classes.

The file then computes the Herbrand quotient of the S-units from that of the group U_{L,∅} of units at every finite place, which Set.unitEmptyEquivUnits identifies with (𝓞 L)ˣ. Recording at each prime w of L above S the valuation of an S-unit (Set.unitValuation) gives an exact sequence of representations of Aut(L/K)

0 → U_{L,∅} → U_{L,S} → ℤ[S_L],

where ℤ[S_L] is the permutation lattice on the primes of L above S. The last map has finite cokernel: the class number of L kills the class of every prime, so its multiple of every vector of ℤ[S_L] is the valuation vector of an S-unit. When the group of K-automorphisms of L is cyclic the Herbrand quotient is therefore multiplicative along the sequence (herbrandQuotient_sUnitsRep_eq_mul), and for a cyclic Galois extension the permutation lattice contributes the local degrees (herbrandQuotient_sUnitsRep):

h(U_{L,S}) = h(U_{L,∅}) · ∏_{v ∈ S} [L_w : K_v].

This is the finite-place part of the Herbrand quotient of the S-units, which enters the computation of the Herbrand quotient h(C_L) = [L : K] of the idele classes. The quotient formula h(C_L) = h(I_{L,S}) / h(U_{L,S}), for S whose primes generate the class group of L, is herbrandQuotient_ideleClassRep.

Main results

• TauCeti.ClassFieldTheory.finite_tateCohomology_zero_sUnitsRep and TauCeti.ClassFieldTheory.finite_tateCohomology_negOne_sUnitsRep: the low-degree Tate groups of the S-units are finite.
• TauCeti.ClassFieldTheory.herbrandQuotient_sUnitsRep_eq_mul: when Aut(L/K) is cyclic, h(U_{L,S}) = h(U_{L,∅}) · h(ℤ[S_L]).
• TauCeti.ClassFieldTheory.herbrandQuotient_sUnitsRep: for cyclic Galois L/K, h(U_{L,S}) = h(U_{L,∅}) · ∏_{v ∈ S} [L_w : K_v].

References

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

theorem TauCeti.ClassFieldTheory.moduleFinite_sUnitsRep {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] : Module.Finite ℤ ↑(sUnitsRep L S)

The integral representation on the S-units of L is finitely generated when S is finite.

theorem TauCeti.ClassFieldTheory.finite_tateCohomology_zero_sUnitsRep {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] : Finite ↑(tateCohomology (sUnitsRep L S) 0)

The degree-zero Tate cohomology of the S-units is finite.

theorem TauCeti.ClassFieldTheory.finite_tateCohomology_negOne_sUnitsRep {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] : Finite ↑(tateCohomology (sUnitsRep L S) (-1))

The degree-minus-one Tate cohomology of the S-units is finite.

The valuation sequence

The Herbrand quotient

theorem TauCeti.ClassFieldTheory.herbrandQuotient_sUnitsRep_eq_mul {K : Type} (L : Type) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) [Finite ↑S] [IsCyclic Gal(L/K)] : TateCohomology.herbrandQuotient (sUnitsRep L S) = TateCohomology.herbrandQuotient (sUnitsRep L ∅) * TateCohomology.herbrandQuotient (Rep.ofMulAction ℤ Gal(L/K) ↑(IsDedekindDomain.HeightOneSpectrum.primesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) S))

The Herbrand quotient of the S-units of an extension L/K of number fields whose group of K-automorphisms is cyclic, for a finite set S of finite places of K, is that of the units at every finite place times that of the permutation lattice on the primes of L above S: h(U_{L,S}) = h(U_{L,∅}) · h(ℤ[S_L]).

theorem TauCeti.ClassFieldTheory.herbrandQuotient_sUnitsRep {K L : Type} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [IsCyclic Gal(L/K)] (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (w : (v : ↥S) → { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver (↑v).asIdeal }) : TateCohomology.herbrandQuotient (sUnitsRep L ↑S) = TateCohomology.herbrandQuotient (sUnitsRep L ∅) * ∏ v : ↥S, ↑(Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑(w v)))

The Herbrand quotient of the S-units of a cyclic Galois extension L/K of number fields, for a finite set S of finite places of K: h(U_{L,S}) = h(U_{L,∅}) · ∏_{v ∈ S} [L_w : K_v], where U_{L,∅} is the group of units at every finite place. The places w above each v may be chosen arbitrarily.