Theorems · Definition · group theory

Rep.coinvariantsMk

(k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] → CategoryTheory.forget₂ (Rep.{u_1, u, v} k G) (ModuleCat k) ⟶ Rep.coinvariantsFunctor k G

The quotient map from a representation to its coinvariants induces a natural transformation from the forgetful functor Rep k G ⥤ ModuleCat k to the coinvariants functor.

Defined in

Mathlib.RepresentationTheory.Coinvariants

Cited by

26 results in Mathlib

Foundations

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

Assumes

CommRingMonoid