Theorems · Theorem · group theory

Rep.coinvariantsFunctor_hom_ext

∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A : Rep.{w, u, v} k G} {M : ModuleCat k}
  {f g : (Rep.coinvariantsFunctor k G).obj A ⟶ M},
  CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) f =
      CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A) g →
    f = g

Defined in

Mathlib.RepresentationTheory.Coinvariants

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingMonoid