Theorems · Theorem · group theory

Representation.freeLift_toLinearMap

∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) {α : Type w'} (f : α → V),
  (σ.freeLift f).toLinearMap =
    (Finsupp.linearCombination k fun x => (σ x.2) (f x.1)) ∘ₗ
      ↑(Finsupp.curryLinearEquiv k).symm ∘ₗ Finsupp.mapRange.linearMap ↑(MonoidAlgebra.coeffLinearEquiv k)

Defined in

Mathlib.RepresentationTheory.Equiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

MonoidAddCommMonoidCommSemiringModule