Herbrand quotients of finite cyclic group representations #
For a representation M of a finite cyclic group, its Herbrand quotient is the quotient of the
orders of H-hat^0(G, M) and H-hat^(-1)(G, M). This file defines it directly on Mathlib's
Tate-cohomology carrier, on top of the low-degree descriptions
H-hat^0(G, M) = M^G / N M and H-hat^(-1)(G, M) = ker(N) / I_G M,
and proves its two base calculations: the quotient is 1 for a finite module, and it is |G|
for the trivial integral representation. Both low-degree Tate groups of a finite module are
finite, since each is a subquotient of the module itself. By two-periodicity it is also the
classical ratio |H²(G, M)| / |H¹(G, M)| of ordinary group cohomology, so that it computes the
order of H²(G, M) whenever H¹(G, M) vanishes.
It then proves that the Herbrand quotient is multiplicative in a short exact sequence. The
argument is the classical exact hexagon: the periodic chain complex of
TauCeti.RepresentationTheory.Homological.TateCohomology.Periodic is a functor of the
coefficients, so a short exact sequence of representations gives a short exact sequence of
complexes and hence a long exact sequence of homology groups, which alternates between the
degree-0 and the degree--1 Tate groups; naturality of the periodicity in odd degrees splices
that sequence into a cycle of six maps. Counting each of the six groups against the image of the
map leaving it and the image of the map entering it gives the identity
|H-hat^0(X₁)| |H-hat^0(X₃)| |H-hat^(-1)(X₂)| = |H-hat^(-1)(X₁)| |H-hat^(-1)(X₃)| |H-hat^0(X₂)|, which is multiplicativity once the
degree--1 orders are known to be nonzero.
The same hexagon gives the invariance of the Herbrand quotient: a short exact sequence with a finite outer term has the same quotient at the two remaining terms, and therefore a morphism with finite kernel and cokernel, factored through its image, leaves the quotient unchanged. Invariance is what lets an arithmetic computation of a Herbrand quotient replace a module by a commensurable one, such as a unit group by a lattice on which the group acts freely. This invariance construction follows E. Artin and J. Tate, Class Field Theory, Chapter IX, section 4.
The proofs are adapted to Mathlib's current Tate complex from the corresponding calculations in
ClassFieldTheory/Cohomology/FiniteCyclic/HerbrandQuotient/{Defs,Finite,Trivial}.lean in
kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509. The trivial
integral calculation reads off the low-degree evaluations
natCard_tateCohomology_zero_trivial_int_eq_card and
subsingleton_tateCohomology_negOne_trivial_int.
Main definitions #
TauCeti.TateCohomology.herbrandQuotientis the Herbrand quotient.TauCeti.TateCohomology.herbrandQuotient_eq_one_of_finitecomputes it for a finite module.TauCeti.TateCohomology.herbrandQuotient_trivial_int_eq_cardcomputes it for trivial integral coefficients.
Main results #
TauCeti.TateCohomology.herbrandQuotient_eq_natCard_H2_div_natCard_H1: the Herbrand quotient is|H²(G, M)| / |H¹(G, M)|;TauCeti.TateCohomology.herbrandQuotient_eq_natCard_H2is the caseH¹(G, M) = 0.TauCeti.TateCohomology.herbrandQuotient_eq_of_iso: isomorphic representations have the same Herbrand quotient.TauCeti.TateCohomology.herbrandQuotient_coind: Shapiro's lemma for Herbrand quotients,h_G(Coind_S^G A) = h_S(A)for a subgroupSof a finite cyclic groupG.TauCeti.TateCohomology.herbrandQuotient_res_of_bijective: restriction along an isomorphism of finite groups does not change the Herbrand quotient.TauCeti.TateCohomology.natCard_tateCohomology_mul_of_shortExact: the exact hexagon of a short exact sequence, in the form of an identity between two products of three orders. It assumes no finiteness.TauCeti.TateCohomology.natCard_tateCohomology_negOne_dvd_of_shortExact: the order of the middle degree--1Tate group divides the product of the two outer ones.TauCeti.TateCohomology.herbrandQuotient_eq_mul_of_shortExact: multiplicativity of the Herbrand quotient in a short exact sequence whose outer terms have finite degree--1Tate cohomology.TauCeti.TateCohomology.herbrandQuotient_eq_of_shortExact_of_finite_X₁andTauCeti.TateCohomology.herbrandQuotient_eq_of_shortExact_of_finite_X₃: a finite outer term of a short exact sequence may be discarded.TauCeti.TateCohomology.herbrandQuotient_eq_of_epi_of_finite_kernelandTauCeti.TateCohomology.herbrandQuotient_eq_of_mono_of_finite_cokernel: the one-sided forms.TauCeti.TateCohomology.herbrandQuotient_eq_of_finite_kernel_of_finite_cokernel: invariance of the Herbrand quotient under a morphism with finite kernel and cokernel.
References #
- J.-P. Serre, Local Fields, Chapter VIII, section 4.
- E. Artin and J. Tate, Class Field Theory, Chapter IX, section 4.
The Herbrand quotient, the order of degree-zero Tate cohomology divided by the order of
degree -1 Tate cohomology. Classically the invariant is only defined when both Tate groups are
finite; this definition is totalized by Nat.card, which is 0 on an infinite type, so together
with division by zero it returns 0 as soon as either group is infinite. The definition makes
sense for any finite group; periodicity makes it useful for cyclic groups.
Equations
- TauCeti.TateCohomology.herbrandQuotient M = ↑(Nat.card ↑(tateCohomology M 0)) / ↑(Nat.card ↑(tateCohomology M (-1)))
Instances For
The Herbrand quotient is the ratio of the orders of degree zero and degree -1 Tate
cohomology. This unfolding equation is deliberately not @[simp]: the terminating evaluations
below keep herbrandQuotient as their left-hand side, and unfolding it first would make each of
them non-simp-normal.
The Herbrand quotient vanishes exactly when one of its two defining Tate groups is infinite.
For a finite representation of a finite cyclic group the two low-degree Tate groups have the same order.
The Herbrand quotient of a finite representation of a finite cyclic group is one.
Isomorphic representations have the same Herbrand quotient.
For a finite cyclic group the Herbrand quotient is the ratio of the orders of ordinary group
cohomology in degrees two and one, h(M) = #H²(G, M) / #H¹(G, M): two-periodicity identifies the
Tate groups of degrees 0 and -1 with those of degrees 2 and 1, which are ordinary group
cohomology.
For a finite cyclic group, if H¹(G, M) vanishes then the Herbrand quotient of M is the
order of H²(G, M). This is how a computation of the Herbrand quotient determines H² once
H¹ is known to vanish, as Hilbert's Theorem 90 gives for the units of a cyclic extension.
The Herbrand quotient of the trivial integral representation is the order of the finite group.
Shapiro's lemma for Herbrand quotients. For a subgroup S of a finite cyclic group G and
a representation A of S, the coinduced representation Coind_S^G A has the same Herbrand
quotient over G as A has over S. Both quotients are ratios |H²| / |H¹| of ordinary group
cohomology, S being cyclic as well, and Shapiro's lemma groupCohomology.coindIso identifies the
cohomology of Coind_S^G A with that of A in every degree.
This computes the Herbrand quotient of a module whose factors are permuted transitively by G
from that of the stabilizer of one factor. For a cyclic extension L/K of number fields and a
place v of K, the module ∏_{w ∣ v} L_wˣ is coinduced in this way from the decomposition group
of one place w acting on L_wˣ.
Restriction along an isomorphism of finite groups does not change the Herbrand quotient.
The exact hexagon in cardinality form. For a short exact sequence of representations of a finite cyclic group, the product of the orders of the Tate groups at three alternate corners of the hexagon equals the product at the other three. No finiteness is assumed: an infinite Tate group makes both sides zero.
In the hexagon, the middle degree -1 Tate group is squeezed between the two outer ones: its
order divides their product. In particular it is finite as soon as they are.
The Herbrand quotient is multiplicative in a short exact sequence. For a short exact
sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of representations of a finite cyclic group whose outer terms
have finite Tate cohomology in degree -1, the Herbrand quotient of the middle term is the
product of the Herbrand quotients of the outer ones. The degree-zero groups are unconstrained:
if one of them is infinite both sides are zero.
A finite outer term on the left may be discarded: if X₁ is finite in a short exact sequence
0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of representations of a finite cyclic group, then X₂ and X₃ have the
same Herbrand quotient. Nothing is assumed about the Tate cohomology of X₂ and X₃: if one of
their Tate groups is infinite, both quotients are 0.
A finite outer term on the right may be discarded: if X₃ is finite in a short exact sequence
0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of representations of a finite cyclic group, then X₂ and X₁ have the
same Herbrand quotient. Nothing is assumed about the Tate cohomology of X₁ and X₂: if one of
their Tate groups is infinite, both quotients are 0.
A surjection with finite kernel does not change the Herbrand quotient.
An injection with finite cokernel does not change the Herbrand quotient.
The Herbrand quotient is invariant under a morphism with finite kernel and cokernel.
For representations of a finite cyclic group, a morphism f : M ⟶ N whose kernel and cokernel
are finite does not change the Herbrand quotient: factoring f through its image, the first
half is a surjection with finite kernel and the second an injection with finite cokernel.