Theorems · Theorem · group theory

Rep.coinvariantsTensor_hom_ext

∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A B : Rep.{u, u, v} k G} {M : ModuleCat k}
  {f g : ((Rep.coinvariantsTensor k G).obj A).obj B ⟶ M},
  (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom f) = (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom g) →
    f = g

Defined in

Mathlib.RepresentationTheory.Coinvariants

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingMonoid