forget_commGrp_preserves_epi — Mathlib

English

The forgetful functor from commutative groups to sets preserves monomorphisms; equivalently, if a morphism is mono in CommGrpCat, its underlying function is injective.

Русский

Функтор забывания из коммутативных групп в множества сохраняет мономорфизмы; следовательно, если морфизм в CommGrpCat является моно, то соответствующая функция инъективна.

LaTeX

$$$$ \operatorname{Mono}(f) \Rightarrow \operatorname{Function.Injective}(f.\mathrm{hom}) $$$$

Lean4

@[to_additive AddCommGrpCat.forget_commGrp_preserves_epi]
instance forget_commGrp_preserves_epi : (forget CommGrpCat).PreservesEpimorphisms where
  preserves f e := by rwa [epi_iff_surjective, ← CategoryTheory.epi_iff_surjective] at e

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