instEpiModuleCatH0π — Mathlib

English

For a k-linear G-representation A, the canonical 0-th group homology map H0π A: H0(G, A) → coinvariants_k G(A) is an epimorphism.

Русский

Для k-линейного представления G-а A каноническое отображение H0(G, A) → A_G (парциальные факторы по эквивалентности) является эпиморфизмом.

LaTeX

$$$\\operatorname{Epi}(H_0\\pi_A).$$$

Lean4

instance : Epi (H0π A) := by unfold H0π; infer_instance

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