Theorems · Definition · group theory

Rep.FiniteCyclicGroup.normHomCompSub

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

Given a finite cyclic group G generated by g : G and a k-linear G-representation A, this is the short complex in ModuleCat k given by A --N--> A --(ρ(g) - 𝟙)--> A where N is the norm map. Its homology is Hⁱ(G, A) for even i and Hᵢ(G, A) for odd i.

Defined in

Mathlib.RepresentationTheory.Homological.FiniteCyclic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingCommGroupFintype