Theorems · Definition · group theory

Rep.linearizationOfMulActionIso

(k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        (H : Type u) →
          [inst_2 : MulAction G H] → (Rep.linearization k G).obj (Action.ofMulAction G H) ≅ Rep.ofMulAction k G H

The linearization of a type H with a G-action is definitionally isomorphic to the k-linear G-representation on k[H] induced by the G-action on H.

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

CommRingMonoidMulAction