Theorems · Definition · group theory

Rep.ihom

{k : Type u} →
  [inst : CommRing k] →
    {G : Type v} →
      [inst_1 : Group G] → Rep.{w, u, v} k G → CategoryTheory.Functor (Rep.{u_1, u, v} k G) (Rep.{max w u_1, u, v} k G)

Given a k-linear G-representation (A, ρ₁), this is the 'internal Hom' functor sending (B, ρ₂) to the representation Homₖ(A, B) that maps g : G and f : A →ₗ[k] B to (ρ₂ g) ∘ₗ f ∘ₗ (ρ₁ g⁻¹).

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingGroup