Theorems · Definition · group theory

Rep.Tor

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

The left-derived functors given by deriving the second argument of A, B ↦ (A ⊗[k] B)_G.

Defined in

Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingGroup