Theorems · Definition · group theory

Rep.coinvariantsTensorFreeToFinsupp

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        (α : Type u) →
          [DecidableEq α] →
            (CategoryTheory.MonoidalCategoryStruct.tensorObj A (Rep.free k G α)).ρ.Coinvariants →ₗ[k] α →₀ ↑A

Given a k-linear G-representation (A, ρ) and a type α, this is the map (A ⊗ (α →₀ k[G]))_G →ₗ[k] (α →₀ A) sending ⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a)).

Defined in

Mathlib.RepresentationTheory.Coinvariants

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingGroupDecidableEq