Tate cohomology of modules induced and coinduced from the trivial subgroup

For a finite group G, every Tate cohomology group of the representation Coind_⊥^G X coinduced from the trivial subgroup vanishes (Milne, Class Field Theory, II 3.1): in positive degrees this is Shapiro's lemma for cohomology, in degrees below -1 Shapiro's lemma for homology (induction and coinduction from the trivial subgroup agree for a finite group), and degrees 0 and -1 are checked by hand. The same holds for Ind_⊥^G X. For a finite subgroup S of an arbitrary group G, the Tate cohomology of S with coefficients in the restrictions of Coind_⊥^G X, Ind_⊥^G X and k[G] vanishes as well. These statements follow ClassFieldTheory/Cohomology/IndCoind/TrivialCohomology.lean in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509.

More generally, Tate cohomology vanishes for every representation whose identity is a norm x ↦ ∑ g, g φ(g⁻¹ x) of a linear map φ, since such an identity factors through Coind_⊥^G. This criterion is stable under reduction modulo a scalar r : k. Hence a representation free of rank one over k[G] remains Tate-trivial modulo r, read as an integral representation. This is the form in which the graded pieces A ⧸ ϖ • A of a Galois-stable lattice A in a local field enter Serre's computation of the Herbrand quotient of its local units (Serre, Local class field theory, VI §1.4).

Main statements

• TauCeti.TateCohomology.isZero_coindBot, TauCeti.TateCohomology.isZero_indBot: for a finite group G, Ĥⁿ(G, Coind_⊥^G X) = 0 and Ĥⁿ(G, Ind_⊥^G X) = 0 for all n : ℤ (Milne II 3.1).
• TauCeti.TateCohomology.isZero_leftRegular: for a finite group G, Ĥⁿ(G, k[G]) = 0.
• TauCeti.TateCohomology.isZero_res_coindBot, TauCeti.TateCohomology.isZero_res_indBot, TauCeti.TateCohomology.isZero_res_leftRegular: for a finite subgroup S of any group G, Ĥⁿ(S, Coind_⊥^G X) = Ĥⁿ(S, Ind_⊥^G X) = Ĥⁿ(S, k[G]) = 0 for all n : ℤ.
• TauCeti.TateCohomology.isZero_of_forall_eq_sum: if the identity of C is a norm x ↦ ∑ g, g φ(g⁻¹ x), then Ĥⁿ(G, C) = 0 for all n : ℤ.
• TauCeti.TateCohomology.isZero_restrictScalarsInt_of_equiv_leftRegular: if V is free of rank one over k[G], then Ĥⁿ(G, V) = 0 over ℤ.
• TauCeti.TateCohomology.isZero_restrictScalarsInt_quotSMulTop_of_equiv_leftRegular: if V is free of rank one over k[G], then Ĥⁿ(G, V ⧸ r • V) = 0 over ℤ for every r : k.

References

• J. S. Milne, Class Field Theory, Chapter II, §3.
• J.-P. Serre, Local class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VI, §1.4.

theorem TauCeti.TateCohomology.isZero_coindBot_zero {k G : Type u} [CommRing k] [Group G] [Fintype G] (X : Type u) [AddCommGroup X] [Module k X] : CategoryTheory.Limits.IsZero (tateCohomology (Rep.coindBot k G X) 0)

Degree-zero Tate cohomology of a representation coinduced from the trivial subgroup vanishes (Milne II 3.1, case r = 0).

theorem TauCeti.TateCohomology.isZero_coindBot_negOne {k G : Type u} [CommRing k] [Group G] [Fintype G] (X : Type u) [AddCommGroup X] [Module k X] : CategoryTheory.Limits.IsZero (tateCohomology (Rep.coindBot k G X) (-1))

Degree -1 Tate cohomology of a representation coinduced from the trivial subgroup vanishes (Milne II 3.1, case r = -1).

theorem TauCeti.TateCohomology.isZero_coindBot {k G : Type u} [CommRing k] [Group G] [Fintype G] (X : Type u) [AddCommGroup X] [Module k X] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.coindBot k G X) n)

For a finite group, all Tate cohomology of a representation coinduced from the trivial subgroup vanishes (Milne II 3.1).

theorem TauCeti.TateCohomology.isZero_indBot {k G : Type u} [CommRing k] [Group G] [Fintype G] (X : Type u) [AddCommGroup X] [Module k X] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.indBot k G X) n)

For a finite group, all Tate cohomology of a representation induced from the trivial subgroup vanishes (Milne II 3.1).

theorem TauCeti.TateCohomology.isZero_leftRegular {k G : Type u} [CommRing k] [Group G] [Fintype G] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.leftRegular k G) n)

For a finite group, all Tate cohomology of the left regular representation k[G] vanishes.

theorem TauCeti.TateCohomology.map_eq_zero_of_hom_apply_eq_sum {k G : Type u} [CommRing k] [Group G] [Fintype G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) (φ : ↑A →ₗ[k] ↑B) (hf : ∀ (x : ↑A), (Rep.Hom.hom f) x = ∑ g : G, (B.ρ g) (φ ((A.ρ g⁻¹) x))) (n : ℤ) : (tateCohomologyFunctor n).map f = 0

For a finite group, a morphism of representations which is the norm x ↦ ∑ g, B.ρ g (φ (A.ρ g⁻¹ x)) of a linear map φ : A → B induces zero on Tate cohomology in every degree: it factors through the coinduced representation Coind_⊥^G A, whose Tate cohomology vanishes.

theorem TauCeti.TateCohomology.isZero_of_forall_eq_sum {k G : Type u} [CommRing k] [Group G] [Fintype G] {C : Rep.{u, u, u} k G} (φ : ↑C →ₗ[k] ↑C) (hφ : ∀ (x : ↑C), x = ∑ g : G, (C.ρ g) (φ ((C.ρ g⁻¹) x))) (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology C n)

If the identity of C is the norm x ↦ ∑ g, C.ρ g (φ (C.ρ g⁻¹ x)) of a k-linear map φ, then all Tate cohomology of C vanishes: the identity of C factors through the coinduced representation Coind_⊥^G C.

theorem TauCeti.TateCohomology.isZero_tensor_of_forall_eq_sum {k G : Type u} [CommRing k] [Group G] [Fintype G] {C : Rep.{u, u, u} k G} (φ : ↑C →ₗ[k] ↑C) (hφ : ∀ (x : ↑C), x = ∑ g : G, (C.ρ g) (φ ((C.ρ g⁻¹) x))) (M : Rep.{u, u, u} k G) (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M C) n)

If the identity of C is the norm x ↦ ∑ g, C.ρ g (φ (C.ρ g⁻¹ x)) of a k-linear map φ, then for every representation M all Tate cohomology of M ⊗ C vanishes: the identity of M ⊗ C is the norm of M ⊗ φ.

theorem TauCeti.TateCohomology.isZero_tensor_coindBot {k G : Type u} [CommRing k] [Group G] [Fintype G] (X : Type u) [AddCommGroup X] [Module k X] (M : Rep.{u, u, u} k G) (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M (Rep.coindBot k G X)) n)

For a finite group and any representation M, all Tate cohomology of M ⊗ Coind_⊥^G X vanishes: the identity of Coind_⊥^G X is the norm of the projection onto the functions supported at 1.

theorem TauCeti.TateCohomology.isZero_tensor_indBot {k G : Type u} [CommRing k] [Group G] [Fintype G] (X : Type u) [AddCommGroup X] [Module k X] (M : Rep.{u, u, u} k G) (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj M (Rep.indBot k G X)) n)

For a finite group and any representation M, all Tate cohomology of M ⊗ Ind_⊥^G X vanishes.

theorem TauCeti.TateCohomology.isZero_res_coindBot {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [Fintype ↥S] (X : Type u) [AddCommGroup X] [Module k X] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype (Rep.coindBot k G X)) n)

For a finite subgroup S of a group G, all Tate cohomology of the restriction to S of a representation coinduced from the trivial subgroup of G vanishes.

theorem TauCeti.TateCohomology.isZero_res_indBot {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [Fintype ↥S] (X : Type u) [AddCommGroup X] [Module k X] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype (Rep.indBot k G X)) n)

For a finite subgroup S of a group G, all Tate cohomology of the restriction to S of a representation induced from the trivial subgroup of G vanishes.

theorem TauCeti.TateCohomology.isZero_res_leftRegular {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [Fintype ↥S] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.res S.subtype (Rep.leftRegular k G)) n)

For a finite subgroup S of a group G, all Tate cohomology of the restriction to S of the left regular representation k[G] vanishes.

Free representations modulo a scalar

This is the graded-piece step of Serre's computation of the Herbrand quotient of the units of a local field (Serre, Local class field theory, VI §1.4).

theorem TauCeti.TateCohomology.isZero_restrictScalarsInt_of_forall_eq_sum {k : Type u_1} {G V : Type} [Group G] [Fintype G] [AddCommGroup V] [Semiring k] [Module k V] {ρ : Representation k G V} (φ : V →ₗ[k] V) (hφ : ∀ (x : V), x = ∑ g : G, (ρ g) (φ ((ρ g⁻¹) x))) (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.of ρ.restrictScalarsInt) n)

If the identity of ρ is the norm x ↦ ∑ g, ρ g (φ (ρ g⁻¹ x)) of a k-linear map φ, then all Tate cohomology of ρ, read as an integral representation, vanishes.

theorem TauCeti.TateCohomology.exists_forall_eq_sum_of_equiv_leftRegular {k : Type u_1} {G V : Type} [Group G] [Fintype G] [AddCommGroup V] [Semiring k] [Module k V] {ρ : Representation k G V} (e : (Representation.leftRegular k G).Equiv ρ) : ∃ (φ : V →ₗ[k] V), ∀ (x : V), x = ∑ g : G, (ρ g) (φ ((ρ g⁻¹) x))

If ρ is free of rank one over the group ring k[G], then the identity of ρ is the norm x ↦ ∑ g, ρ g (φ (ρ g⁻¹ x)) of a k-linear map φ: the projection onto the coefficient of 1 ∈ G.

theorem TauCeti.TateCohomology.isZero_restrictScalarsInt_of_equiv_leftRegular {k : Type u_1} {G V : Type} [Group G] [Fintype G] [AddCommGroup V] [Semiring k] [Module k V] {ρ : Representation k G V} (e : (Representation.leftRegular k G).Equiv ρ) (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.of ρ.restrictScalarsInt) n)

If ρ is free of rank one over the group ring k[G], then all Tate cohomology of ρ, read as an integral representation, vanishes.

theorem TauCeti.TateCohomology.isZero_restrictScalarsInt_quotSMulTop_of_forall_eq_sum {k : Type u_1} {G V : Type} [Group G] [Fintype G] [AddCommGroup V] [CommRing k] [Module k V] {ρ : Representation k G V} (φ : V →ₗ[k] V) (hφ : ∀ (x : V), x = ∑ g : G, (ρ g) (φ ((ρ g⁻¹) x))) (r : k) (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.of (ρ.quotSMulTop r).restrictScalarsInt) n)

If the identity of ρ is the norm x ↦ ∑ g, ρ g (φ (ρ g⁻¹ x)) of a k-linear map φ, then for every r : k all Tate cohomology of the reduction V ⧸ r • V, as an integral representation, vanishes: its identity is the norm of the reduction of φ.

theorem TauCeti.TateCohomology.isZero_restrictScalarsInt_quotSMulTop_of_equiv_leftRegular {k : Type u_1} {G V : Type} [Group G] [Fintype G] [AddCommGroup V] [CommRing k] [Module k V] {ρ : Representation k G V} (e : (Representation.leftRegular k G).Equiv ρ) (r : k) (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (Rep.of (ρ.quotSMulTop r).restrictScalarsInt) n)

A free representation modulo a scalar has trivial Tate cohomology. If ρ is free of rank one over the group ring k[G], then for every r : k all Tate cohomology of the reduction V ⧸ r • V, a free module of rank one over (k ⧸ (r))[G], read as an integral representation, vanishes. Its identity is the norm of the reduction of the projection onto the coefficient of 1 ∈ G.