Theorems · Definition · group theory

groupHomology.cycles

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

The n-cycles Zₙ(G, A) of a k-linear G-representation A, i.e. the kernel of the differential Cₙ(G, A) ⟶ Cₙ₋₁(G, A) in the complex of inhomogeneous chains.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Cited by

66 results in Mathlib

Foundations

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

Assumes

CommRingGroup