instEpiModuleCatAppActionCoinvariantsMk

English

For every G‑representation X over k, the canonical map from X to its coinvariants X_G is surjective; i.e., the morphism realizing coinvariants is an epimorphism in the module category.

Русский

Для любой G‑представления X над кольцом k каноническое отображение X → X_G является сюръекцией; то есть отображение, описывающее coinvariants, является эпиморфизмом в модульной категории.

LaTeX

$$$\forall X \;\operatorname{surj}((\mathrm{coinvariantsMk}\ k\ G).\mathrm{app} X)$$$

Lean4

instance (X : Rep k G) : Epi ((coinvariantsMk k G).app X) :=
  (ModuleCat.epi_iff_surjective _).2 <| Representation.Coinvariants.mk_surjective X.ρ

Похожие утверждения