Theorems · Definition · group theory

Rep.FiniteCyclicGroup.moduleCatCochainComplex

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

Given a finite cyclic group G generated by g : G and a k-linear G-representation A, this is the periodic chain complex in Rep k G given by 0 ⟶ A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A --N--> A ⟶ ... where N is the norm map. Its cohomology is the group cohomology of A.

Defined in

Mathlib.RepresentationTheory.Homological.FiniteCyclic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommGroupFintype