π — Mathlib · SciLib

English

The nth group cohomology is isomorphic to Ext^n in the category of k-linear G-representations, with k considered as the trivial G-representation.

Русский

Пусть k—кольцо, G—группа. Тогда n-я когомология группы изоморфна Ext^n(k, A) в категории k- линейных представлений G, где k трактуется как тривиальное представление G.

LaTeX

$$$$ groupCohomology A n \\cong (\\mathrm{Ext}\\ k(\\mathrm{Rep}\\ kG)\\ n).obj A. $$$$

Lean4

/-- The natural map from `n`-cocycles to `n`th group cohomology for a `k`-linear
`G`-representation `A`. -/
abbrev π [Group G] (A : Rep k G) (n : ℕ) : groupCohomology.cocycles A n ⟶ groupCohomology A n :=
  (inhomogeneousCochains A).homologyπ n

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