Tate cohomology of a product of representations

Let G be a finite group and M i a family of representations of G, indexed by an arbitrary type ι. This file shows that Tate cohomology commutes with the product Rep.pi M in every integer degree:

H-hat^n(G, ∏ i, M i) ≃ ∏ i, H-hat^n(G, M i),

the i-th component being induced by the projection onto M i (linearEquivPi).

Degrees 0 and -1 rest on the low-degree descriptions H-hat^0 = Mᴳ / N_G M and H-hat^(-1) = ker N_G / I_G M, where invariants, norms and the augmentation submodule I_G M of a product are all computed componentwise. For the norm image and the augmentation submodule this needs a choice in every factor at once, and for the latter also the finiteness of G (Representation.mem_coinvariantsKer_pi_iff). By Tate's triviality criterion, which needs only two consecutive degrees on the subgroups of prime-power order, a product of cohomologically trivial representations is then cohomologically trivial (isZero_res_pi). The products of the dimension-shifting sequences 0 → M i → Coind_⊥^G (M i) → ⋯ → 0 and 0 → ⋯ → Ind_⊥^G (M i) → M i → 0 are short exact with cohomologically trivial middle terms, so their connecting maps, which are natural in the projections, carry the low-degree computation to every degree.

Consequently the Herbrand quotient of a product is the product of the Herbrand quotients of the factors, as soon as all but finitely many factors have trivial Tate cohomology in degrees 0 and -1. This is the shape of the S-ideles of a Galois extension L/K of number fields: they are the product over the places v of K of the Galois modules ∏_{w ∣ v} L_wˣ for v ∈ S and ∏_{w ∣ v} 𝒪_wˣ for v ∉ S, and the factors of the second kind are cohomologically trivial when L/K is unramified at v.

Main definitions

• TauCeti.TateCohomology.linearEquivPi: H-hat^n(G, ∏ i, M i) ≃ ∏ i, H-hat^n(G, M i) for every n : ℤ.

Main results

• TauCeti.TateCohomology.linearEquivPi_zero_H0π and TauCeti.TateCohomology.linearEquivPi_negOne_HNegOneπ: in degrees 0 and -1 the equivalence sends the class of an element to the family of the classes of its components.
• TauCeti.TateCohomology.isZero_res_pi: a product of cohomologically trivial representations is cohomologically trivial.
• TauCeti.TateCohomology.herbrandQuotient_pi: h(∏ i, M i) = ∏ i ∈ s, h(M i) when the factors outside the finite set s have trivial Tate cohomology in degrees 0 and -1.

References

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

Degree zero

Degree minus one

Products of cohomologically trivial representations

theorem TauCeti.TateCohomology.isZero_res_pi {R G ι : Type u} [CommRing R] [Group G] (M : ι → Rep.{u, u, u} R G) [Finite G] (hM : ∀ (i : ι) (S : Subgroup G) [inst : Fintype ↥S] (n : ℤ), CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype (M i)) n)) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype (Rep.pi M)) n)

A product of cohomologically trivial representations is cohomologically trivial. By Tate's triviality criterion it suffices to check degrees -1 and 0 on the subgroups of prime-power order, where the Tate cohomology of the product is the product of the Tate cohomologies.

theorem TauCeti.TateCohomology.isZero_pi {R G ι : Type u} [CommRing R] [Group G] [Fintype G] (M : ι → Rep.{u, u, u} R G) (hM : ∀ (i : ι) (S : Subgroup G) [inst : Fintype ↥S] (n : ℤ), CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype (M i)) n)) (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.pi M) n)

A product of cohomologically trivial representations has vanishing Tate cohomology.

Every degree

noncomputable def TauCeti.TateCohomology.linearEquivPi {R G ι : Type u} [CommRing R] [Group G] [Fintype G] (M : ι → Rep.{u, u, u} R G) (n : ℤ) : ↑(tateCohomology (Rep.pi M) n) ≃ₗ[R] (i : ι) → ↑(tateCohomology (M i) n)

Tate cohomology commutes with products in every integer degree: H-hat^n(G, ∏ i, M i) ≃ ∏ i, H-hat^n(G, M i), the i-th component being induced by the projection onto M i.

@[simp]

theorem TauCeti.TateCohomology.linearEquivPi_apply {R G ι : Type u} [CommRing R] [Group G] [Fintype G] (M : ι → Rep.{u, u, u} R G) (n : ℤ) (x : ↑(tateCohomology (Rep.pi M) n)) (i : ι) : (linearEquivPi M n) x i = (ModuleCat.Hom.hom ((tateCohomologyFunctor n).map (Rep.piProj M i))) x

The i-th component of linearEquivPi is induced by the projection onto M i.

theorem TauCeti.TateCohomology.linearEquivPi_zero_H0π {R G ι : Type u} [CommRing R] [Group G] [Fintype G] (M : ι → Rep.{u, u, u} R G) (y : ↥(Rep.pi M).ρ.invariants) (i : ι) : (linearEquivPi M 0) ((CategoryTheory.ConcreteCategory.hom (H0π (Rep.pi M))) y) i = (CategoryTheory.ConcreteCategory.hom (H0π (M i))) ⟨↑y i, ⋯⟩

In degree 0, linearEquivPi sends the class of an invariant element of the product to the family of the classes of its components.

theorem TauCeti.TateCohomology.linearEquivPi_negOne_HNegOneπ {R G ι : Type u} [CommRing R] [Group G] [Fintype G] (M : ι → Rep.{u, u, u} R G) (y : ↥(LinearMap.ker (Rep.pi M).ρ.norm)) (i : ι) : (linearEquivPi M (-1)) ((CategoryTheory.ConcreteCategory.hom (HNegOneπ (Rep.pi M))) y) i = (CategoryTheory.ConcreteCategory.hom (HNegOneπ (M i))) ⟨↑y i, ⋯⟩

In degree -1, linearEquivPi sends the class of a norm-zero element of the product to the family of the classes of its components.

The Herbrand quotient of a product

theorem TauCeti.TateCohomology.herbrandQuotient_pi {R G ι : Type u} [CommRing R] [Group G] [Fintype G] (M : ι → Rep.{u, u, u} R G) (s : Finset ι) (h0 : ∀ i ∉ s, Subsingleton ↑(tateCohomology (M i) 0)) (h1 : ∀ i ∉ s, Subsingleton ↑(tateCohomology (M i) (-1))) : herbrandQuotient (Rep.pi M) = ∏ i ∈ s, herbrandQuotient (M i)

The Herbrand quotient of a product of representations of a finite group is the product of the Herbrand quotients of the factors, when the factors outside a finite set s have trivial Tate cohomology in degrees 0 and -1. In particular, for a finite index type it is the product of all the Herbrand quotients.