Theorems · Definition · group theory

Rep.FiniteCyclicGroup.chainComplexFunctor

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

Given a finite group G and g : G, this is the functor Rep k G ⥤ ChainComplex (Rep k G) ℕ sending A : Rep k G to the periodic chain complex in Rep k G given by ... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0 where N is the norm map. When G is generated by g and A is the left regular representation k[G], it is a projective resolution of k as a trivial representation. It sends a morphism f : A ⟶ B to the chain morphism defined by f in every degree.

Defined in

Mathlib.RepresentationTheory.Homological.FiniteCyclic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingCommGroupFintype