Theorems · Definition · group theory

groupCohomology.H0Iso

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → groupCohomology.H0 A ≅ ModuleCat.of k ↥A.ρ.invariants

The 0th group cohomology of A, defined as the 0th cohomology of the complex of inhomogeneous cochains, is isomorphic to the invariants of the representation on A.

Defined in

Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommRingGroup