Theorems · Definition · group theory

Rep.linearizationTrivialIso

(k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        (X : Type u) → (Rep.linearization k G).obj (Action.trivial G X) ≅ Rep.trivial k G (MonoidAlgebra k X)

The linearization of a type X on which G acts trivially is the trivial G-representation on k[X].

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingMonoid