Theorems · Definition · group theory

Rep.FiniteCyclicGroup.moduleCatChainComplex

{k G : Type u} →
  [inst : CommRing k] → [inst_1 : CommGroup G] → [Fintype G] → Rep.{u_1, u, u} k G → G → ChainComplex (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 ModuleCat k given by ... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0 where N is the norm map. Its homology is the group homology 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