Theorems · Definition · group theory

groupHomology.inhomogeneousChains

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

Given a k-linear G-representation A, this is the complex of inhomogeneous chains $$\dots \to \bigoplus_{G^1} A \to \bigoplus_{G^0} A \to 0$$ which calculates the group homology of A.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Cited by

90 results in Mathlib

Foundations

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

Assumes

CommRingGroup