isZero_groupCohomology_succ_of_subsingleton

English

If G is a subsingleton (trivial group), then for any A the higher group cohomology vanishes: the (n+1)st cohomology is zero.

Русский

Если G является тривиальной группой, то когомологии в положительных степенях нулевые: H^{n+1}(G,A) = 0.

LaTeX

$$$$ \\text{If } G \\text{ is subsingleton, then } groupCohomology A (n+1) \\cong 0. $$$$

Lean4

theorem isZero_groupCohomology_succ_of_subsingleton [Group G] [Subsingleton G] (A : Rep k G) (n : ℕ) :
    Limits.IsZero (groupCohomology A (n + 1)) :=
  (isZero_Ext_succ_of_projective (Rep.trivial k G k) A n).of_iso <| groupCohomologyIsoExt _ _

Похожие утверждения