Theorems · Definition · group theory

groupCohomology.inhomogeneousCochains

{k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → CochainComplex (ModuleCat k) ℕ

Given a k-linear G-representation A, this is the complex of inhomogeneous cochains $$0 \to \mathrm{Fun}(G^0, A) \to \mathrm{Fun}(G^1, A) \to \mathrm{Fun}(G^2, A) \to \dots$$ which calculates the group cohomology of A.

Defined in

Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Cited by

83 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingGroup