Low-degree Tate cohomology and Herbrand quotients of permutation modules

Let a finite group G act on a type X, and let R[X] be the permutation representation Rep.ofMulAction R G X. This file computes its Tate cohomology in degrees 0 and -1.

• In degree -1 it vanishes as soon as multiplication by |G| is injective on R (for instance when R has no additive torsion): an element of norm zero has orbit sums killed by |G|, hence zero orbit sums, and so lies in the augmentation submodule.
• In degree 0, for X finite, it is ∏_ω R ⧸ (|G_ω|), the product over the orbits ω of the quotient of R by the order of the stabilizer of a point of ω. An invariant vector is constant on every orbit, and the norm of the basis vector at a point x is |G_x| times the indicator of its orbit.

Consequently the Herbrand quotient of ℤ[X] is ∏_ω |G_ω|. For a transitive action it is the order of a point stabilizer, and for X = G ⧸ H it is |H|: the Herbrand quotient of the module induced from the trivial H-module ℤ is that of the trivial module, as Shapiro's lemma predicts. No cyclicity is needed for these computations.

This is the lattice side of the computation of the Herbrand quotient of the S-units of a cyclic extension of number fields L/K: there X is the set of places of L above a finite set S of places of K, the stabilizers are the decomposition groups, and the Herbrand quotient of ℤ[X] is the product of the local degrees.

Main definitions

• TauCeti.TateCohomology.H0LinearEquivPiQuotientStabilizer: for X finite, H-hat^0(G, R[X]) ≃ ∏_ω R ⧸ (|G_ω|).

Main results

• TauCeti.TateCohomology.subsingleton_tateCohomology_negOne_ofMulAction_of_isSMulRegular: H-hat^(-1)(G, R[X]) = 0 when multiplication by |G| is injective on R.
• TauCeti.TateCohomology.subsingleton_tateCohomology_negOne_ofMulAction: the instance H-hat^(-1)(G, R[X]) = 0 when R has no additive torsion.
• TauCeti.TateCohomology.natCard_tateCohomology_zero_ofMulAction: |H-hat^0(G, ℤ[X])| = ∏_ω |G_ω|.
• TauCeti.TateCohomology.herbrandQuotient_ofMulAction: h(ℤ[X]) = ∏_ω |G_ω|.
• TauCeti.TateCohomology.herbrandQuotient_ofMulAction_of_isPretransitive: h(ℤ[X]) = |G_x| for a transitive action.
• TauCeti.TateCohomology.herbrandQuotient_ofMulAction_sum: multiplicativity over a disjoint union.
• TauCeti.TateCohomology.herbrandQuotient_ofMulAction_sigma: multiplicativity over a finite sigma family with finite fibre orbit spaces.
• TauCeti.TateCohomology.herbrandQuotient_ofMulAction_sigma_of_isPretransitive: the product of the stabilizer orders for a finite family of transitive actions.
• TauCeti.TateCohomology.herbrandQuotient_ofMulAction_quotient: h(ℤ[G ⧸ H]) = |H|.

References

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

theorem TauCeti.TateCohomology.subsingleton_tateCohomology_negOne_ofMulAction_of_isSMulRegular {R G X : Type u} [CommRing R] [Group G] [MulAction G X] [Fintype G] (hR : IsSMulRegular R (Fintype.card G)) : Subsingleton ↑(tateCohomology (Rep.ofMulAction R G X) (-1))

Degree -1 Tate cohomology of a permutation module vanishes as soon as multiplication by |G| is injective on the coefficient ring.

instance TauCeti.TateCohomology.subsingleton_tateCohomology_negOne_ofMulAction {R G X : Type u} [CommRing R] [Group G] [MulAction G X] [Fintype G] [HasUniqueDiv R] : Subsingleton ↑(tateCohomology (Rep.ofMulAction R G X) (-1))

Degree -1 Tate cohomology of a permutation module vanishes over a coefficient ring without additive torsion.

noncomputable def TauCeti.TateCohomology.H0LinearEquivPiQuotientStabilizer (R G X : Type u) [CommRing R] [Group G] [MulAction G X] [Fintype G] [Finite X] : ↑(tateCohomology (Rep.ofMulAction R G X) 0) ≃ₗ[R] (ω : MulAction.orbitRel.Quotient G X) → R ⧸ Ideal.span {↑(Nat.card ↥(MulAction.stabilizer G (Quotient.out ω)))}

Degree-zero Tate cohomology of a permutation module. For a finite G-set X, H-hat^0(G, R[X]) is the product over the orbits ω of R ⧸ (|G_ω|), where G_ω is the stabilizer of the chosen representative of ω. A class is sent to the residues of the coefficients of an invariant representative at the orbit representatives (H0LinearEquivPiQuotientStabilizer_H0π).

@[simp]

theorem TauCeti.TateCohomology.H0LinearEquivPiQuotientStabilizer_H0π {R G X : Type u} [CommRing R] [Group G] [MulAction G X] [Fintype G] [Finite X] (v : ↥(Rep.ofMulAction R G X).ρ.invariants) (ω : MulAction.orbitRel.Quotient G X) : (H0LinearEquivPiQuotientStabilizer R G X) ((CategoryTheory.ConcreteCategory.hom (H0π (Rep.ofMulAction R G X))) v) ω = (Ideal.Quotient.mk (Ideal.span {↑(Nat.card ↥(MulAction.stabilizer G (Quotient.out ω)))})) ((↑v).coeff (Quotient.out ω))

The degree-zero equivalence sends the class of an invariant vector to the residues of its coefficients at the orbit representatives.

theorem TauCeti.TateCohomology.natCard_tateCohomology_zero_ofMulAction {G X : Type} [Group G] [Fintype G] [MulAction G X] [Fintype (MulAction.orbitRel.Quotient G X)] : Nat.card ↑(tateCohomology (Rep.ofMulAction ℤ G X) 0) = ∏ ω : MulAction.orbitRel.Quotient G X, Nat.card ↥(MulAction.stabilizer G (Quotient.out ω))

The order of H-hat^0(G, ℤ[X]) is the product over the orbits of the orders of the stabilizers.

theorem TauCeti.TateCohomology.herbrandQuotient_ofMulAction {G X : Type} [Group G] [Fintype G] [MulAction G X] [Fintype (MulAction.orbitRel.Quotient G X)] : herbrandQuotient (Rep.ofMulAction ℤ G X) = ∏ ω : MulAction.orbitRel.Quotient G X, ↑(Nat.card ↥(MulAction.stabilizer G (Quotient.out ω)))

The Herbrand quotient of a permutation module ℤ[X] is the product over the orbits of the orders of the stabilizers.

theorem TauCeti.TateCohomology.herbrandQuotient_ofMulAction_of_isPretransitive {G X : Type} [Group G] [Fintype G] [MulAction G X] [MulAction.IsPretransitive G X] (x : X) : herbrandQuotient (Rep.ofMulAction ℤ G X) = ↑(Nat.card ↥(MulAction.stabilizer G x))

For a transitive action, the Herbrand quotient of ℤ[X] is the order of a point stabilizer.

theorem TauCeti.TateCohomology.herbrandQuotient_ofMulAction_sum {G X Y : Type} [Group G] [Fintype G] [MulAction G X] [MulAction G Y] [Finite (MulAction.orbitRel.Quotient G X)] [Finite (MulAction.orbitRel.Quotient G Y)] : herbrandQuotient (Rep.ofMulAction ℤ G (X ⊕ Y)) = herbrandQuotient (Rep.ofMulAction ℤ G X) * herbrandQuotient (Rep.ofMulAction ℤ G Y)

The Herbrand quotient of a permutation lattice on a disjoint union is the product of those of its two summands. No cyclicity is needed.

theorem TauCeti.TateCohomology.herbrandQuotient_ofMulAction_sigma {G ι : Type} {X : ι → Type} [Group G] [Fintype G] [Fintype ι] [(i : ι) → MulAction G (X i)] [∀ (i : ι), Finite (MulAction.orbitRel.Quotient G (X i))] : herbrandQuotient (Rep.ofMulAction ℤ G ((i : ι) × X i)) = ∏ i : ι, herbrandQuotient (Rep.ofMulAction ℤ G (X i))

The Herbrand quotient of a permutation lattice on a finite sigma family is the product of the Herbrand quotients of its fibres, provided each fibre has finitely many orbits.

theorem TauCeti.TateCohomology.herbrandQuotient_ofMulAction_sigma_of_isPretransitive {G ι : Type} {X : ι → Type} [Group G] [Fintype G] [Fintype ι] [(i : ι) → MulAction G (X i)] [∀ (i : ι), MulAction.IsPretransitive G (X i)] (x : (i : ι) → X i) : herbrandQuotient (Rep.ofMulAction ℤ G ((i : ι) × X i)) = ∏ i : ι, ↑(Nat.card ↥(MulAction.stabilizer G (x i)))

For a finite family of nonempty transitive actions, the Herbrand quotient of the permutation lattice is the product of the stabilizer orders, one for each fibre.

theorem TauCeti.TateCohomology.herbrandQuotient_ofMulAction_quotient {G : Type} [Group G] [Fintype G] (H : Subgroup G) : herbrandQuotient (Rep.ofMulAction ℤ G (G ⧸ H)) = ↑(Nat.card ↥H)

The Herbrand quotient of ℤ[G ⧸ H], the module induced from the trivial H-module ℤ, is |H|.