Theorems · Definition · group theory

Rep.finsuppTensorRight

(k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        (A B : Rep.{u, u, v} k G) →
          (α : Type u) →
            [DecidableEq α] →
              CategoryTheory.MonoidalCategoryStruct.tensorObj A (Rep.finsupp α B) ≅
                Rep.finsupp α (CategoryTheory.MonoidalCategoryStruct.tensorObj A B)

Given representations A, B and a type α, this is the natural representation isomorphism A ⊗ (α →₀ B) ≅ (A ⊗ B) →₀ α sending a ⊗ₜ single x b ↦ single x (a ⊗ₜ b).

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingMonoidDecidableEq