Theorems · Definition · group theory

Rep.coinvariantsTensorIndIso

{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) →
              (B : Rep.{u, u, u} k H) →
                ((Rep.coinvariantsTensor k H).obj (Rep.ind φ A)).obj B ≅
                  ((Rep.coinvariantsTensor k G).obj A).obj (Rep.res φ B)

Given a group hom φ : G →* H, A : Rep k G and B : Rep k H, this is the k-linear isomorphism (Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G sending ⟦h ⊗ₜ a⟧ ⊗ₜ b to ⟦a ⊗ ρ(h)(b)⟧ for all h : H, a : A, and b : B.

Defined in

Mathlib.RepresentationTheory.Induced

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingGroupGroup