Theorems · Definition · group theory

Rep.coinvariantsTensor

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

The functor sending A, B to (A ⊗[k] B)_G. This is naturally isomorphic to the functor sending A, B to A ⊗[k[G]] B, where we give A the k[G]ᵐᵒᵖ-module structure defined by g • a := A.ρ g⁻¹ a.

Defined in

Mathlib.RepresentationTheory.Coinvariants

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommRingMonoid