English
Let A and B be representations of G over k and f: A → B a morphism. Then f is an epimorphism in the representation category if and only if the underlying linear map f.hom is surjective.
Русский
Пусть A и B — представления группы G над полем k и f: A → B — морфизм. Тогда f является эпиморфизмом в категории представлений тогда и только тогда, когда соответствующая линейная карта f.hom сюръективна.
LaTeX
$$$\mathrm{Epi}(f) \iff \operatorname{Surjective}(f_{\mathrm{hom}})$$$
Lean4
theorem epi_iff_surjective {A B : Rep k G} (f : A ⟶ B) : Epi f ↔ Function.Surjective f.hom :=
⟨fun _ => (ModuleCat.epi_iff_surjective ((forget₂ _ _).map f)).1 inferInstance, fun h =>
(forget₂ _ _).epi_of_epi_map ((ModuleCat.epi_iff_surjective <| (forget₂ _ _).map f).2 h)⟩
