Theorems · Definition · group theory

Rep.RepToAction

(k : Type u) →
  (G : Type v) →
    [inst : Ring k] → [inst_1 : Monoid G] → CategoryTheory.Functor (Rep.{w, u, v} k G) (Action (ModuleCat k) G)

Every object in Rep k G naturally correspond to an object in Action.

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

4 results in Mathlib

Foundations

Depth 53 from the axioms · uses propext, Quot.sound

Assumes

RingMonoid