Theorems · Definition · group theory

HomologicalComplex.coinvariantsTensorObj

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {α : Type u_1} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] → Rep.{u, u, u} k G → ChainComplex (Rep.{u, u, u} k G) α → ChainComplex (ModuleCat k) α

Given A : Rep k G and a chain complex P in Rep k G, this is the chain complex whose nth object is (A ⊗ Pₙ)_G.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingGroupAddRightCancelSemigroupOne