Cohomologically trivial representations have projective dimension at most one

Let G be a finite group and k a principal ideal domain of characteristic zero in which every prime number is a unit or generates a maximal ideal, such as ℤ, ℤ_[p], ℤ_(p) or a field of characteristic zero. If a representation A of G over k is cohomologically trivial, that is, its Tate cohomology vanishes in every degree on every subgroup of G, then the kernel of every surjection onto A from a projective k[G]-module is projective (Rim, Ann. of Math. 69 (1959); Brown, Cohomology of Groups, VI §8). Every module is a quotient of a free one, so every cohomologically trivial A has a projective resolution of length one, with no finiteness hypothesis on A. In the other direction, projective representations are cohomologically trivial (Rep.isZero_res_of_projective).

For the free k[G]-module F on the elements of A, the kernel R of F ↠ A is a k-submodule of the free k-module F, hence free over k (Submodule.free_of_isPrincipalIdealRing). It is cohomologically trivial by the long exact sequence, since F and A are, so it is projective by the lattice form of the theorem, Rep.projective_of_isZero_res. By Schanuel's lemma (LinearMap.projective_ker_of_projective_ker) the kernel of any other surjection onto A from a projective module, in any universe, is then projective too.

The resolution of length one makes cohomological triviality stable under tensor products: if A is cohomologically trivial and Tor₁^k(M, A) = 0, then M ⊗ A, with the diagonal action, is cohomologically trivial (Nakayama, Ann. of Math. 65 (1957)), because tensoring 0 → R → F → A → 0 with M stays exact and M ⊗ R, M ⊗ F are cohomologically trivial (Rep.isZero_res_tensor_of_shortExact). This is how the theorem of Nakayama and Rim enters the Tate–Nakayama generalization of Tate's theorem, an isomorphism from the Tate cohomology of M in degree r to that of M ⊗ C in degree r + 2, for a class module C with Tor₁^ℤ(M, C) = 0, whose splitting module is cohomologically trivial. The vanishing of Tor₁^k(M, A) is stated without a Tor functor, in the equivalent form that M ⊗ - keeps injective the first map of every short exact sequence 0 → X → Y → A → 0 of k-modules; it holds when M is flat over k and when A is.

Main statements

• Rep.projective_ker_of_isZero_res: if A is cohomologically trivial, every surjection onto A.ρ.asModule from a projective k[G]-module has projective kernel.
• Rep.isZero_res_tensor_of_isZero_res: if A is cohomologically trivial and Tor₁^k(M, A) = 0, then M ⊗ A is cohomologically trivial.
• Rep.isZero_res_tensor_of_isZero_res_of_flat_left, Rep.isZero_res_tensor_of_isZero_res_of_flat_right: the same when M, respectively A, is flat over k.

References

• D. S. Rim, Modules over finite groups, Ann. of Math. 69 (1959).
• K. S. Brown, Cohomology of Groups, Chapter VI, §8.
• J.-P. Serre, Local Fields, Chapter IX, §§3–5.
• T. Nakayama, Cohomology of class field theory and tensor product modules I, Ann. of Math. 65 (1957).

theorem Rep.projective_ker_of_isZero_res {k G : Type u} [CommRing k] [Group G] [Finite G] [IsDomain k] [IsPrincipalIdealRing k] [CharZero k] (hk : ∀ (p : ℕ), Nat.Prime p → IsUnit ↑p ∨ (Ideal.span {↑p}).IsMaximal) (A : Rep.{u, u, u} k G) (hA : ∀ (S : Subgroup G) [inst : Fintype ↥S] (n : ℤ), CategoryTheory.Limits.IsZero (tateCohomology (res S.subtype A) n)) {P : Type u_1} [AddCommGroup P] [Module (MonoidAlgebra k G) P] [Module.Projective (MonoidAlgebra k G) P] (f : P →ₗ[MonoidAlgebra k G] A.ρ.asModule) (hf : Function.Surjective ⇑f) : Module.Projective (MonoidAlgebra k G) ↥f.ker

Nakayama–Rim: cohomological triviality gives projective dimension at most one. If A is cohomologically trivial, the kernel of every surjection onto A.ρ.asModule from a projective k[G]-module is projective. Here k is a principal ideal domain of characteristic zero in which every prime number is a unit or generates a maximal ideal; no finiteness is assumed of A or of the projective module.

theorem Rep.isZero_res_tensor_of_isZero_res {k G : Type u} [CommRing k] [Group G] [Finite G] [IsDomain k] [IsPrincipalIdealRing k] [CharZero k] (hk : ∀ (p : ℕ), Nat.Prime p → IsUnit ↑p ∨ (Ideal.span {↑p}).IsMaximal) (A : Rep.{u, u, u} k G) (hA : ∀ (S : Subgroup G) [inst : Fintype ↥S] (n : ℤ), CategoryTheory.Limits.IsZero (tateCohomology (res S.subtype A) n)) (M : Rep.{u, u, u} k G) (hM : ∀ {X Y : Type u} [inst : AddCommGroup X] [inst_1 : Module k X] [inst_2 : AddCommGroup Y] [inst_3 : Module k Y] (f : X →ₗ[k] Y) (g : Y →ₗ[k] ↑A), Function.Injective ⇑f → Function.Exact ⇑f ⇑g → Function.Surjective ⇑g → Function.Injective ⇑(LinearMap.lTensor (↑M) f)) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (res S.subtype (CategoryTheory.MonoidalCategoryStruct.tensorObj M A)) n)

Tensoring with a cohomologically trivial module. Let k be a principal ideal domain of characteristic zero in which every prime number is a unit or generates a maximal ideal, and let A be a cohomologically trivial representation of a finite group G over k. If Tor₁^k(M, A) = 0, in the form that M ⊗ X → M ⊗ Y is injective for every short exact sequence 0 → X → Y → A → 0 of k-modules, then M ⊗ A is cohomologically trivial.

theorem Rep.isZero_res_tensor_of_isZero_res_of_flat_left {k G : Type u} [CommRing k] [Group G] [Finite G] [IsDomain k] [IsPrincipalIdealRing k] [CharZero k] (hk : ∀ (p : ℕ), Nat.Prime p → IsUnit ↑p ∨ (Ideal.span {↑p}).IsMaximal) (A : Rep.{u, u, u} k G) (hA : ∀ (S : Subgroup G) [inst : Fintype ↥S] (n : ℤ), CategoryTheory.Limits.IsZero (tateCohomology (res S.subtype A) n)) (M : Rep.{u, u, u} k G) [Module.Flat k ↑M] (S : Subgroup G) [Fintype ↥S] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (res S.subtype (CategoryTheory.MonoidalCategoryStruct.tensorObj M A)) n)

Tensoring a cohomologically trivial module with a flat module. Over k as in Rep.isZero_res_tensor_of_isZero_res, if A is cohomologically trivial and M is flat over k, then M ⊗ A is cohomologically trivial.

theorem Rep.isZero_res_tensor_of_isZero_res_of_flat_right {k G : Type u} [CommRing k] [Group G] [Finite G] [IsDomain k] [IsPrincipalIdealRing k] [CharZero k] (hk : ∀ (p : ℕ), Nat.Prime p → IsUnit ↑p ∨ (Ideal.span {↑p}).IsMaximal) (A : Rep.{u, u, u} k G) [Module.Flat k ↑A] (hA : ∀ (S : Subgroup G) [inst : Fintype ↥S] (n : ℤ), CategoryTheory.Limits.IsZero (tateCohomology (res S.subtype A) n)) (M : Rep.{u, u, u} k G) (S : Subgroup G) [Fintype ↥S] (n : ℤ) : CategoryTheory.Limits.IsZero (tateCohomology (res S.subtype (CategoryTheory.MonoidalCategoryStruct.tensorObj M A)) n)

Tensoring a flat cohomologically trivial module. Over k as in Rep.isZero_res_tensor_of_isZero_res, if A is cohomologically trivial and flat over k, then M ⊗ A is cohomologically trivial for every representation M.