Theorems · Definition · group theory

Rep.coinvariantsTensorIndNatIso

{k : Type u} →
  [inst : CommRing k] →
    {G H : Type u} →
      [inst_1 : Group G] →
        [inst_2 : Group H] →
          (φ : G →* H) →
            (A : Rep.{u, u, u} k G) →
              (Rep.coinvariantsTensor k H).obj (Rep.ind φ A) ≅
                (Rep.resFunctor φ).comp ((Rep.coinvariantsTensor k G).obj A)

Given a group hom φ : G →* H and A : Rep k G, the functor Rep k H ⥤ ModuleCat k sending B ↦ (Ind(φ)(A) ⊗ B))_H is naturally isomorphic to the one sending B ↦ (A ⊗ Res(φ)(B))_G.

Defined in

Mathlib.RepresentationTheory.Induced

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroup