Theorems · Definition · group theory

groupHomology.coinvariantsTensorResProjectiveResolutionIso

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (S : Subgroup G) →
        (A : Rep.{u, u, u} k ↥S) →
          (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) →
            HomologicalComplex.coinvariantsTensorObj A ((Rep.resFunctor S.subtype).mapProjectiveResolution P).complex ≅
              HomologicalComplex.coinvariantsTensorObj (Rep.ind S.subtype A) P.complex

Given a projective resolution P of k as a k-linear G-representation, a subgroup S ≤ G, and a k-linear S-representation A, this is an isomorphism of complexes (A ⊗ Res(S)(P))_S ≅ (Ind_S^G(A) ⊗ P)_G.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroup