Theorems · Definition · group theory

Rep.freeLiftLEquiv

(k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] → (α : Type u') → (A : Rep.{max (max u u') v, u, v} k G) → (Rep.free k G α ⟶ A) ≃ₗ[k] α → ↑A

The natural linear equivalence between functions α → A and representation morphisms (α →₀ k[G]) ⟶ A.

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingMonoid