English
Let A,B be G‑representations with B arbitrary. For any M, if two morphisms f,g : (coinvariants k G).obj A ⟶ M agree after precomposition with the coinvariants projection, then f and g are equal. This expresses that coinvariants form an epi‑cancellation domain for maps out of A.
Русский
Пусть A,B — G‑представления, M — модуль. Если две гомоморфизмы f,g: (coinvariants k G).obj A ⟶ M совпадают после предварительного композиции с аплайком coinvariants Mk A, то они равны. Это выражает свойство сокращения по coinvariants.
LaTeX
$$$\forall M:\text{ModuleCat}(k),\;\forall f,g:\big((\mathrm{coinvariantsFunctor}\ k\ G).\mathrm{obj} A\to M\big),\;((\mathrm{coinvariantsMk}\ k\ G).\mathrm{app} A \;\gg f = (\mathrm{coinvariantsMk}\ k\ G).\mathrm{app} A \;\gg g) \Rightarrow f=g$$
Lean4
@[ext]
theorem coinvariantsFunctor_hom_ext {M : ModuleCat k} {f g : (coinvariantsFunctor k G).obj A ⟶ M}
(hfg : (coinvariantsMk k G).app A ≫ f = (coinvariantsMk k G).app A ≫ g) : f = g :=
(cancel_epi _).1 hfg
