Theorems · Definition · group theory

Rep.tensorHomEquiv

{k : Type u} →
  [inst : CommRing k] →
    {G : Type v} →
      [inst_1 : Group G] →
        (A B C : Rep.{u, u, v} k G) → (CategoryTheory.MonoidalCategoryStruct.tensorObj A B ⟶ C) ≃ (B ⟶ A.ihom.obj C)

Given a k-linear G-representation A, this is the Hom-set bijection in the adjunction A ⊗ - ⊣ ihom(A, -). It sends f : A ⊗ B ⟶ C to a Rep k G morphism defined by currying the k-linear map underlying f, giving a map A →ₗ[k] B →ₗ[k] C, then flipping the arguments.

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

4 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Quot.sound

Assumes

CommRingGroup