Theorems · Definition · group theory

Rep.diagonalHomEquiv

(k G : Type u) →
  [inst : Group G] →
    [inst_1 : CommRing k] → (n : ℕ) → (A : Rep.{u, u, u} k G) → (Rep.diagonal k G (n + 1) ⟶ A) ≃ₗ[k] (Fin n → G) → ↑A

Given a k-linear G-representation A, the set of representation morphisms Hom(k[Gⁿ⁺¹], A) is k-linearly isomorphic to the set of functions Gⁿ → A.

Defined in

Mathlib.RepresentationTheory.Rep.Iso

Cited by

0 results in Mathlib

Foundations

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

Assumes

GroupCommRing